[isabelle] use_thy "Pure";
In an attempt to build the raw Isabelle process,
I am trying to get my ML system to make sense of this file:
It goes fine till the point when its given
upon when it complains with the following.
Loading theory "Pure
*** Uninitialized theory data "Isar/attributes"
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.
I am wondering if any of you have ever done something like this before
and if you can help.
I will be very grateful for any info on the sequence of function calls
involved in "use_thy" and the dependecies.
Thanks in advance for your help,
This archive was generated by a fusion of
Pipermail (Mailman edition) and