author | clasohm |
Thu, 16 Sep 1993 16:25:32 +0200 | |
changeset 2 | c67f44be880f |
parent 1 | c6a6e3db5353 |
child 3 | 5f77582e3a89 |
src/Pure/ROOT.ML | file | annotate | diff | comparison | revisions |
--- a/src/Pure/ROOT.ML Thu Sep 16 14:21:44 1993 +0200 +++ b/src/Pure/ROOT.ML Thu Sep 16 16:25:32 1993 +0200 @@ -28,11 +28,6 @@ use "ROOT.ML"; cd ".."; -(* Theory parser *) -cd "Thy"; -use "ROOT.ML"; -cd ".."; - print_depth 1; use "type.ML"; use "sign.ML"; @@ -69,3 +64,9 @@ open Basic_Syntax Thm Drule Tactical Tactic Goals; structure Pure = struct val thy = pure_thy end; + +(* Theory parser *) +cd "Thy"; +use "ROOT.ML"; +cd ".."; +