removed Isar/proof_history.ML;
authorwenzelm
Mon, 14 Jul 2008 11:19:36 +0200
changeset 27559 14b238b1000c
parent 27558 33f215fa079e
child 27560 8e46cf4fe26c
removed Isar/proof_history.ML; added Isar/proof_node.ML
src/Pure/IsaMakefile
src/Pure/Isar/ROOT.ML
--- a/src/Pure/IsaMakefile	Mon Jul 14 11:04:47 2008 +0200
+++ b/src/Pure/IsaMakefile	Mon Jul 14 11:19:36 2008 +0200
@@ -41,7 +41,7 @@
   Isar/obtain.ML Isar/outer_keyword.ML Isar/outer_lex.ML		\
   Isar/outer_parse.ML Isar/outer_syntax.ML Isar/overloading.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/proof_node.ML Isar/rule_cases.ML Isar/rule_insts.ML		\
   Isar/session.ML Isar/skip_proof.ML Isar/spec_parse.ML			\
   Isar/specification.ML Isar/subclass.ML Isar/theory_target.ML		\
   Isar/toplevel.ML ML-Systems/alice.ML ML-Systems/exn.ML		\
--- a/src/Pure/Isar/ROOT.ML	Mon Jul 14 11:04:47 2008 +0200
+++ b/src/Pure/Isar/ROOT.ML	Mon Jul 14 11:19:36 2008 +0200
@@ -69,7 +69,7 @@
 use "constdefs.ML";
 
 (*toplevel transactions*)
-use "proof_history.ML";
+use "proof_node.ML";
 use "toplevel.ML";
 
 (*theory syntax*)