added Isar/specification.ML;
authorwenzelm
Sat Jan 07 23:27:52 2006 +0100 (2006-01-07)
changeset 186133cdfa57408be
parent 18612 7300f75028dc
child 18614 3618d5ae0ac8
added Isar/specification.ML;
src/Pure/IsaMakefile
src/Pure/Isar/ROOT.ML
     1.1 --- a/src/Pure/IsaMakefile	Sat Jan 07 23:27:51 2006 +0100
     1.2 +++ b/src/Pure/IsaMakefile	Sat Jan 07 23:27:52 2006 +0100
     1.3 @@ -42,7 +42,7 @@
     1.4    Isar/outer_keyword.ML Isar/outer_lex.ML Isar/outer_parse.ML                   \
     1.5    Isar/outer_syntax.ML Isar/proof.ML Isar/proof_context.ML                      \
     1.6    Isar/proof_display.ML Isar/proof_history.ML Isar/rule_cases.ML                \
     1.7 -  Isar/session.ML Isar/skip_proof.ML Isar/term_style.ML                         \
     1.8 +  Isar/session.ML Isar/skip_proof.ML Isar/specification.ML Isar/term_style.ML	\
     1.9    Isar/thy_header.ML Isar/toplevel.ML ML-Systems/cpu-timer-basis.ML             \
    1.10    ML-Systems/cpu-timer-gc.ML ML-Systems/polyml-posix.ML                         \
    1.11    ML-Systems/polyml-time-limit.ML ML-Systems/polyml.ML                          \
     2.1 --- a/src/Pure/Isar/ROOT.ML	Sat Jan 07 23:27:51 2006 +0100
     2.2 +++ b/src/Pure/Isar/ROOT.ML	Sat Jan 07 23:27:52 2006 +0100
     2.3 @@ -22,6 +22,7 @@
     2.4  use "induct_attrib.ML";
     2.5  
     2.6  (*derived theory and proof elements*)
     2.7 +use "specification.ML";
     2.8  use "constdefs.ML";
     2.9  use "obtain.ML";
    2.10  use "locale.ML";