Am 27/05/2013 18:13, schrieb Makarius:
> On Mon, 27 May 2013, Stefan Berghofer wrote:
>
>> As I pointed out in my previous mail, it is an error to supply disagreement
>> pairs to unify containing Vars that have the same name but different types.
>> So
>> I don't think one should change pattern.ML
In the meanwhile I had a first look at the implementation of the
"notation" command. Some things I noted w.r.t. localizing ad-hoc
overloading (please correct me if I'm wrong):
- For Overload_Data instead of Theory_Data, I should use Generic_Data
(such that it is available in top-level theories
Hopefully it is all a bit more precise now. Maybe someone wants to
formalize pattern.ML + unify.ML after > 20 years, to pin down the
remaining uncertaincies about type instantiation within these
non-trivial algorithms.
Just for the record, I would be interested in joining such an endeavor.
Unfor
Am 27/05/2013 19:54, schrieb Makarius:
> On Mon, 27 May 2013, Makarius wrote:
>
>> The change ensures that variables with equal name are unified, in the same
>> manner as the types of Free or Const are unified, before doing the real work
>> of HO-unification.
>
> Here is another example for Isabe
On Mon, 27 May 2013, Makarius wrote:
The change ensures that variables with equal name are unified, in the
same manner as the types of Free or Const are unified, before doing the
real work of HO-unification.
Here is another example for Isabelle/Pure, without schematic variables
with differen
On 05/27/2013 05:26 PM, Makarius wrote:
Anyway, after 2-3 more rounds of investigation, I've found more profound
weaknesses of pattern.ML and unify.ML concerning unification of types. This
could lead to situations as sketched above, where types of variables were not
properly instantiated. E.g
On Thu, 2 May 2013, Lawrence Paulson wrote:
I am getting a lot of poly/ML segmentation faults, and they are making
it very difficult to do my work, especially as my theories take at least
15 minutes to load. If it then simply crashes then I'm not getting
anywhere.
Does this still happen? Th
Hi,
in 40fe6b80b481, I stumbled upon the following behaviour. Consider
the following example:
locale Foo = fixes a :: 'a
notepad begin
interpret Foo b for b .
term b
end
jEdit tells me about b in the term command:
term
fixed "b"
skolem variable
:: 'b
So the b from the "
