changeset 7680 | 27bbbe36d49a |
parent 7021 | 0073aa571502 |
child 7728 | 2e737ce3cdb5 |
--- a/src/Pure/Isar/ROOT.ML Fri Oct 01 20:39:40 1999 +0200 +++ b/src/Pure/Isar/ROOT.ML Fri Oct 01 20:40:03 1999 +0200 @@ -19,6 +19,7 @@ use "local_defs.ML"; use "calculation.ML"; use "skip_proof.ML"; +use "obtain.ML"; (*outer syntax*) use "comment.ML"; @@ -52,6 +53,7 @@ structure LocalDefs = LocalDefs; structure Calculation = Calculation; structure SkipProof = SkipProof; + structure Obtain = Obtain; structure Comment = Comment; structure OuterLex = OuterLex; structure OuterParse = OuterParse;