removed isar.ML;
authorwenzelm
Sat, 23 Apr 2005 19:50:15 +0200
changeset 15827 5fdf2d8dab9c
parent 15826 e9b4c9feb296
child 15828 ad483e324b59
removed isar.ML; removed structure PureIsar;
src/Pure/Isar/ROOT.ML
--- a/src/Pure/Isar/ROOT.ML	Sat Apr 23 19:50:05 2005 +0200
+++ b/src/Pure/Isar/ROOT.ML	Sat Apr 23 19:50:15 2005 +0200
@@ -27,7 +27,6 @@
 use "skip_proof.ML";
 
 (*outer syntax*)
-(*use "outer_lex.ML";*)   (*see ../Thy/ROOT.ML*)
 use "antiquote.ML";
 use "outer_parse.ML";
 
@@ -45,40 +44,3 @@
 use "constdefs.ML";
 use "isar_cmd.ML";
 use "isar_syn.ML";
-
-(*main ML interfaces*)
-use "isar.ML";
-
-structure PureIsar =
-struct
-  structure ObjectLogic = ObjectLogic;
-  structure AutoBind = AutoBind;
-  structure RuleCases = RuleCases;
-  structure ProofContext = ProofContext;
-  structure ContextRules = ContextRules;
-  structure Args = Args;
-  structure Attrib = Attrib;
-  structure Locale = Locale;
-  structure Proof = Proof;
-  structure ProofHistory = ProofHistory;
-  structure NetRules = NetRules;
-  structure InductAttrib = InductAttrib;
-  structure Method = Method;
-  structure Calculation = Calculation;
-  structure Obtain = Obtain;
-  structure SkipProof = SkipProof;
-  structure OuterLex = OuterLex;
-  structure Antiquote = Antiquote;
-  structure OuterParse = OuterParse;
-  structure Toplevel = Toplevel;
-  structure Session = Session;
-  structure IsarOutput = IsarOutput;
-  structure ThyHeader = ThyHeader;
-  structure OuterSyntax = OuterSyntax;
-  structure IsarThy = IsarThy;
-  structure Constdefs = Constdefs;
-  structure IsarCmd = IsarCmd;
-  structure IsarSyn = IsarSyn;
-  structure Isar = Isar;
-end;
-