[isabelle-dev] isabelle-dev and ML files

[Makarius]

On Mon, 26 Oct 2009, Timothy Bourke wrote:

>>> I get the following results for Isabelle 2009 and a recent (yesterday)
>>> dev version:
>>>      \            version
>>>  test \     2009          dev
>>>        +-------------+------------+
>>>    ML  |  s1 fails   |  s1 fails  |
>>>        |  s2 works   |  s2 works  |
>>>        +-------------+------------+
>>>    USE |  s1 works   |  s1 works  |
>>>        |  s2 works   |  s2 fails  |
>>>        +-------------+------------+
>>>
>>> Is the dev behaviour correct?
>>
>> Shouldn't the status of s1 and s2 be swapped in ML/dev?
>
> I'm reasonably sure that the table is accurate.

>> The 'ML' and 'use' commands operate exactly the same way, and
>> invoking the "use" function from the raw ML toplevel should coincide
>> with that.

Now I understand that with "ML" in the table you mean the raw Poly/ML 
toplevel.  This is not under our control, so it will be the same 
independently of the Isabelle version.


 	Makarius