--- a/src/Pure/Isar/calculation.ML Sat Jan 25 18:18:03 2014 +0100
+++ b/src/Pure/Isar/calculation.ML Sat Jan 25 18:34:05 2014 +0100
@@ -95,11 +95,11 @@
(* concrete syntax *)
val _ = Theory.setup
- (Attrib.setup (Binding.name "trans") (Attrib.add_del trans_add trans_del)
+ (Attrib.setup @{binding trans} (Attrib.add_del trans_add trans_del)
"declaration of transitivity rule" #>
- Attrib.setup (Binding.name "sym") (Attrib.add_del sym_add sym_del)
+ Attrib.setup @{binding sym} (Attrib.add_del sym_add sym_del)
"declaration of symmetry rule" #>
- Attrib.setup (Binding.name "symmetric") (Scan.succeed symmetric)
+ Attrib.setup @{binding symmetric} (Scan.succeed symmetric)
"resolution with symmetry rule" #>
Global_Theory.add_thms
[((Binding.empty, transitive_thm), [trans_add]),
@@ -197,4 +197,32 @@
val moreover = collect false;
val ultimately = collect true;
+
+(* outer syntax *)
+
+val calc_args =
+ Scan.option (@{keyword "("} |-- Parse.!!! ((Parse_Spec.xthms1 --| @{keyword ")"})));
+
+val _ =
+ Outer_Syntax.command @{command_spec "also"} "combine calculation and current facts"
+ (calc_args >> (Toplevel.proofs' o also_cmd));
+
+val _ =
+ Outer_Syntax.command @{command_spec "finally"}
+ "combine calculation and current facts, exhibit result"
+ (calc_args >> (Toplevel.proofs' o finally_cmd));
+
+val _ =
+ Outer_Syntax.command @{command_spec "moreover"} "augment calculation by current facts"
+ (Scan.succeed (Toplevel.proof' moreover));
+
+val _ =
+ Outer_Syntax.command @{command_spec "ultimately"}
+ "augment calculation by current facts, exhibit result"
+ (Scan.succeed (Toplevel.proof' ultimately));
+
+val _ =
+ Outer_Syntax.improper_command @{command_spec "print_trans_rules"} "print transitivity rules"
+ (Scan.succeed (Toplevel.unknown_context o Toplevel.keep (print_rules o Toplevel.context_of)));
+
end;
--- a/src/Pure/Isar/isar_syn.ML Sat Jan 25 18:18:03 2014 +0100
+++ b/src/Pure/Isar/isar_syn.ML Sat Jan 25 18:34:05 2014 +0100
@@ -688,30 +688,6 @@
Toplevel.skip_proof (fn i => i + 1)));
-(* calculational proof commands *)
-
-val calc_args =
- Scan.option (@{keyword "("} |-- Parse.!!! ((Parse_Spec.xthms1 --| @{keyword ")"})));
-
-val _ =
- Outer_Syntax.command @{command_spec "also"} "combine calculation and current facts"
- (calc_args >> (Toplevel.proofs' o Calculation.also_cmd));
-
-val _ =
- Outer_Syntax.command @{command_spec "finally"}
- "combine calculation and current facts, exhibit result"
- (calc_args >> (Toplevel.proofs' o Calculation.finally_cmd));
-
-val _ =
- Outer_Syntax.command @{command_spec "moreover"} "augment calculation by current facts"
- (Scan.succeed (Toplevel.proof' Calculation.moreover));
-
-val _ =
- Outer_Syntax.command @{command_spec "ultimately"}
- "augment calculation by current facts, exhibit result"
- (Scan.succeed (Toplevel.proof' Calculation.ultimately));
-
-
(* proof navigation *)
val _ =
@@ -847,11 +823,6 @@
Toplevel.keep (Context_Rules.print_rules o Toplevel.context_of)));
val _ =
- Outer_Syntax.improper_command @{command_spec "print_trans_rules"} "print transitivity rules"
- (Scan.succeed (Toplevel.unknown_context o
- Toplevel.keep (Calculation.print_rules o Toplevel.context_of)));
-
-val _ =
Outer_Syntax.improper_command @{command_spec "print_methods"} "print methods of this theory"
(Scan.succeed (Toplevel.unknown_theory o
Toplevel.keep (Method.print_methods o Toplevel.theory_of)));
--- a/src/Pure/Pure.thy Sat Jan 25 18:18:03 2014 +0100
+++ b/src/Pure/Pure.thy Sat Jan 25 18:34:05 2014 +0100
@@ -103,6 +103,7 @@
begin
ML_file "Isar/isar_syn.ML"
+ML_file "Isar/calculation.ML"
ML_file "Tools/rail.ML"
ML_file "Tools/rule_insts.ML";
ML_file "Tools/find_theorems.ML"
--- a/src/Pure/ROOT Sat Jan 25 18:18:03 2014 +0100
+++ b/src/Pure/ROOT Sat Jan 25 18:34:05 2014 +0100
@@ -106,7 +106,6 @@
"Isar/attrib.ML"
"Isar/auto_bind.ML"
"Isar/bundle.ML"
- "Isar/calculation.ML"
"Isar/class.ML"
"Isar/class_declaration.ML"
"Isar/code.ML"
--- a/src/Pure/ROOT.ML Sat Jan 25 18:18:03 2014 +0100
+++ b/src/Pure/ROOT.ML Sat Jan 25 18:34:05 2014 +0100
@@ -236,9 +236,6 @@
use "Isar/method.ML";
use "Isar/proof.ML";
use "Isar/element.ML";
-
-(*derived theory and proof elements*)
-use "Isar/calculation.ML";
use "Isar/obtain.ML";
(*local theories and targets*)