added Isar/theory_target.ML;
authorwenzelm
Sat, 07 Oct 2006 01:31:08 +0200
changeset 20880 b853d4326894
parent 20879 ac46f01024be
child 20881 54481abec257
added Isar/theory_target.ML;
src/Pure/IsaMakefile
src/Pure/Isar/ROOT.ML
--- a/src/Pure/IsaMakefile	Sat Oct 07 01:31:07 2006 +0200
+++ b/src/Pure/IsaMakefile	Sat Oct 07 01:31:08 2006 +0200
@@ -41,7 +41,7 @@
   Isar/outer_syntax.ML Isar/proof.ML Isar/proof_context.ML			\
   Isar/proof_display.ML Isar/proof_history.ML Isar/rule_cases.ML 		\
   Isar/rule_insts.ML Isar/session.ML Isar/skip_proof.ML Isar/specification.ML	\
-  Isar/term_style.ML Isar/thy_header.ML Isar/toplevel.ML			\
+  Isar/term_style.ML Isar/theory_target.ML Isar/thy_header.ML Isar/toplevel.ML	\
   ML-Systems/cpu-timer-basis.ML ML-Systems/cpu-timer-gc.ML			\
   ML-Systems/polyml-4.1.4-patch.ML ML-Systems/polyml-4.2.0.ML			\
   ML-Systems/polyml-4.9.1.ML ML-Systems/polyml-interrupt-timeout.ML		\
--- a/src/Pure/Isar/ROOT.ML	Sat Oct 07 01:31:07 2006 +0200
+++ b/src/Pure/Isar/ROOT.ML	Sat Oct 07 01:31:08 2006 +0200
@@ -33,11 +33,12 @@
 use "induct_attrib.ML";
 
 (*derived theory and proof elements*)
+use "local_theory.ML";
 use "calculation.ML";
 use "obtain.ML";
 use "locale.ML";
 use "../axclass.ML";
-use "local_theory.ML";
+use "theory_target.ML";
 use "specification.ML";
 use "constdefs.ML";