# HG changeset patch
# User wenzelm
# Date 1390671245 -3600
# Node ID 863b4f9f6bd7191691e89a4b7e1b6df85e970ce1
# Parent  7eb0c04e4c40e1284447fd094276dce667b5899a
prefer self-contained user-space tool;

diff -r 7eb0c04e4c40 -r 863b4f9f6bd7 src/Pure/Isar/calculation.ML
--- 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;
diff -r 7eb0c04e4c40 -r 863b4f9f6bd7 src/Pure/Isar/isar_syn.ML
--- 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)));
diff -r 7eb0c04e4c40 -r 863b4f9f6bd7 src/Pure/Pure.thy
--- 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"
diff -r 7eb0c04e4c40 -r 863b4f9f6bd7 src/Pure/ROOT
--- 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"
diff -r 7eb0c04e4c40 -r 863b4f9f6bd7 src/Pure/ROOT.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*)