# HG changeset patch
# User wenzelm
# Date 961969667 -7200
# Node ID f85564116be10376cb326038eaf55c82aa6b4186
# Parent  c702e212527094c959854ac42e1c5a8920774ed6
added Isar/antiquote.ML, Isar/isar_output.ML, Isar/thy_header.ML;

diff -r c702e2125270 -r f85564116be1 src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Sun Jun 25 23:47:12 2000 +0200
+++ b/src/Pure/IsaMakefile	Sun Jun 25 23:47:47 2000 +0200
@@ -28,14 +28,14 @@
   General/object.ML General/path.ML General/position.ML			\
   General/pretty.ML General/scan.ML General/seq.ML General/source.ML	\
   General/symbol.ML General/table.ML General/url.ML Interface/ROOT.ML	\
-  Interface/isamode.ML Interface/proof_general.ML Isar/ROOT.ML		\
+  Interface/isamode.ML Interface/proof_general.ML Isar/ROOT.ML Isar/antiquote.ML \
   Isar/args.ML Isar/attrib.ML Isar/auto_bind.ML Isar/calculation.ML	\
-  Isar/comment.ML Isar/isar.ML Isar/isar_cmd.ML Isar/isar_syn.ML	\
-  Isar/isar_thy.ML Isar/local_defs.ML Isar/method.ML Isar/net_rules.ML	\
-  Isar/obtain.ML Isar/outer_lex.ML Isar/outer_parse.ML			\
+  Isar/comment.ML Isar/isar.ML Isar/isar_cmd.ML Isar/isar_output.ML     \
+  Isar/isar_syn.ML Isar/isar_thy.ML Isar/local_defs.ML Isar/method.ML   \
+  Isar/net_rules.ML Isar/obtain.ML Isar/outer_lex.ML Isar/outer_parse.ML \
   Isar/outer_syntax.ML Isar/proof.ML Isar/proof_context.ML		\
   Isar/proof_data.ML Isar/proof_history.ML Isar/rule_cases.ML		\
-  Isar/session.ML Isar/skip_proof.ML Isar/toplevel.ML			\
+  Isar/session.ML Isar/skip_proof.ML Isar/thy_header.ML Isar/toplevel.ML \
   ML-Systems/mlworks.ML ML-Systems/polyml.ML ML-Systems/smlnj-0.93.ML	\
   ML-Systems/smlnj.ML ROOT.ML Syntax/ROOT.ML Syntax/ast.ML		\
   Syntax/lexicon.ML Syntax/mixfix.ML Syntax/parser.ML			\
diff -r c702e2125270 -r f85564116be1 src/Pure/Isar/ROOT.ML
--- a/src/Pure/Isar/ROOT.ML	Sun Jun 25 23:47:12 2000 +0200
+++ b/src/Pure/Isar/ROOT.ML	Sun Jun 25 23:47:47 2000 +0200
@@ -24,19 +24,22 @@
 use "skip_proof.ML";
 
 (*outer syntax*)
+(*use "outer_lex.ML";*)	  (*see ../Thy/ROOT.ML*)
+use "antiquote.ML";
 use "comment.ML";
-(*use "outer_lex.ML";*)	  (*see ../Thy/ROOT.ML*)
 use "outer_parse.ML";
 
 (*toplevel environment*)
 use "toplevel.ML";
 use "session.ML";
+use "isar_output.ML";
 
 (*theory and proof operations*)
 use "isar_thy.ML";
 use "isar_cmd.ML";
 
 (*theory syntax*)
+use "thy_header.ML";
 use "outer_syntax.ML";
 use "isar_syn.ML";
 
@@ -56,13 +59,16 @@
   structure LocalDefs = LocalDefs;
   structure Calculation = Calculation;
   structure SkipProof = SkipProof;
+  structure OuterLex = OuterLex;
+  structure Antiquote = Antiquote;
   structure Comment = Comment;
-  structure OuterLex = OuterLex;
   structure OuterParse = OuterParse;
   structure Toplevel = Toplevel;
   structure Session = Session;
   structure IsarThy = IsarThy;
+  structure IsarOutput = IsarOutput;
   structure IsarCmd = IsarCmd;
+  structure ThyHeader = ThyHeader;
   structure OuterSyntax = OuterSyntax;
   structure IsarSyn = IsarSyn;
   structure Isar = Isar;