Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
added Isar/rule_insts.ML;
authorwenzelm
Thu, 03 Aug 2006 17:30:41 +0200
changeset 20333 9b406cb9d010
parent 20332 27e4f43a0c3e
child 20334 60157137a0eb
added Isar/rule_insts.ML;
src/Pure/IsaMakefile file | annotate | diff | comparison | revisions
src/Pure/Isar/ROOT.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/IsaMakefile	Thu Aug 03 17:30:40 2006 +0200
+++ b/src/Pure/IsaMakefile	Thu Aug 03 17:30:41 2006 +0200
@@ -39,8 +39,8 @@
   Isar/method.ML Isar/net_rules.ML Isar/object_logic.ML Isar/obtain.ML		\
   Isar/outer_keyword.ML Isar/outer_lex.ML Isar/outer_parse.ML			\
   Isar/outer_syntax.ML Isar/proof.ML Isar/proof_context.ML			\
-  Isar/proof_display.ML Isar/proof_history.ML Isar/rule_cases.ML		\
-  Isar/session.ML Isar/skip_proof.ML Isar/specification.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			\
   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			\
--- a/src/Pure/Isar/ROOT.ML	Thu Aug 03 17:30:40 2006 +0200
+++ b/src/Pure/Isar/ROOT.ML	Thu Aug 03 17:30:41 2006 +0200
@@ -61,6 +61,7 @@
 use "outer_syntax.ML";
 
 (*theory and proof operations*)
+use "rule_insts.ML";
 use "../simplifier.ML";
 use "find_theorems.ML";
 use "isar_thy.ML";
isabelle