# HG changeset patch # User wenzelm # Date 882030436 -3600 # Node ID ad74412ef7a0d15ee2e3607113002894fcc3d432 # Parent 7d4e2832b791ecb9a992406c2ed4f1daa15773d8 version = "Isabelle98: Jan 1998"; diff -r 7d4e2832b791 -r ad74412ef7a0 src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Sat Dec 13 17:22:41 1997 +0100 +++ b/src/Pure/ROOT.ML Sat Dec 13 17:27:16 1997 +0100 @@ -8,7 +8,7 @@ *) val banner = "Pure Isabelle"; -val version = "Isabelle-94 revision 8: May 1997"; +val version = "Isabelle98: Jan 1998"; print_depth 1; @@ -23,7 +23,7 @@ use "ROOT.ML"; cd ".."; -(*Core system*) +(*Main system*) use "sorts.ML"; use "type_infer.ML"; use "type.ML"; @@ -46,10 +46,7 @@ use "axclass.ML"; (*Theory parser and loader*) - -(* FIXME tmp *) -val global_names = ref false; - +val global_names = ref false; (* FIXME tmp *) cd "Thy"; use "ROOT.ML"; cd "..";