Re: [isabelle] use_thy "Pure";



On Tue, 12 Dec 2006, Priya Gopalan wrote:

> I have made some changes to the source inorder to suit the dialect of ML 
> that I am using (alice). I have been trying to investigate if this error 
> is because of
> 
> (1)-any of the changes that i have made
> (2)-of the implementation features of alice
> 
> I can say that (2) is not the case, as i have tried the same experiment 
> (with the same source) in the SML-NJ system and i get the same error.

Maybe you can show your changes to the sources in order to get an idea 
what is going on here.


> I will be very grateful for any info on the sequence of function calls 
> involved in "use_thy" and the dependecies.

The final use_thy "Pure" of the Isabelle bootstrap depends on almost 
everything defined before.


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.