# HG changeset patch
# User wenzelm
# Date 1136672872 -3600
# Node ID 3cdfa57408be832ef9aebf80ad0fe93f6255b4e4
# Parent  7300f75028dc225f687051d4c3f2535f7bc5bc7c
added Isar/specification.ML;

diff -r 7300f75028dc -r 3cdfa57408be src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Sat Jan 07 23:27:51 2006 +0100
+++ b/src/Pure/IsaMakefile	Sat Jan 07 23:27:52 2006 +0100
@@ -42,7 +42,7 @@
   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/term_style.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-posix.ML                         \
   ML-Systems/polyml-time-limit.ML ML-Systems/polyml.ML                          \
diff -r 7300f75028dc -r 3cdfa57408be src/Pure/Isar/ROOT.ML
--- a/src/Pure/Isar/ROOT.ML	Sat Jan 07 23:27:51 2006 +0100
+++ b/src/Pure/Isar/ROOT.ML	Sat Jan 07 23:27:52 2006 +0100
@@ -22,6 +22,7 @@
 use "induct_attrib.ML";
 
 (*derived theory and proof elements*)
+use "specification.ML";
 use "constdefs.ML";
 use "obtain.ML";
 use "locale.ML";