[isabelle] (no subject)
I am compiling Isabelle using a flavour of ML called alice.
While loading the ROOT.ML file (src/Pure/ROOT.ML) at the alice ML shell-level,
it interprets most of it fine, and gets stuck at the point when the
following is invoked:
use_thy "Pure"; structure Pure = struct val thy = theory "Pure" end;
use_thy "CPure"; structure CPure = struct val thy = theory "CPure" end;
Here are the details:
On giving the shell
with this message:
Loading theory "Pure"
*** Uninitialized theory data "Isar/attributes"
*** At command "lemma" (line 18 of
I will be grateful for any info on the possible reasons for a message
like this and how it can be fixed.
This archive was generated by a fusion of
Pipermail (Mailman edition) and