Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
ObtainFun;
authorwenzelm
Wed, 05 Jan 2000 11:42:02 +0100
changeset 8091 226dcdc3c5f3
parent 8090 5a241706d9b3
child 8092 badbfb6ceac0
ObtainFun;
src/Pure/Isar/ROOT.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/ROOT.ML	Wed Jan 05 11:41:38 2000 +0100
+++ b/src/Pure/Isar/ROOT.ML	Wed Jan 05 11:42:02 2000 +0100
@@ -19,7 +19,6 @@
 use "local_defs.ML";
 use "calculation.ML";
 use "skip_proof.ML";
-use "obtain.ML";
 
 (*outer syntax*)
 use "comment.ML";
@@ -30,7 +29,7 @@
 use "toplevel.ML";
 use "session.ML";
 
-(*theory operations*)
+(*theory and proof operations*)
 use "isar_thy.ML";
 use "isar_cmd.ML";
 
@@ -38,7 +37,8 @@
 use "outer_syntax.ML";
 use "isar_syn.ML";
 
-(*main ML interface*)
+(*main ML interfaces*)
+use "obtain.ML";
 use "isar.ML";
 
 structure PureIsar =
@@ -53,7 +53,6 @@
   structure LocalDefs = LocalDefs;
   structure Calculation = Calculation;
   structure SkipProof = SkipProof;
-  structure Obtain = Obtain;
   structure Comment = Comment;
   structure OuterLex = OuterLex;
   structure OuterParse = OuterParse;
isabelle