prefer self-contained user-space tool;
authorwenzelm
Sat Jan 25 18:34:05 2014 +0100 (2014-01-25)
changeset 55141863b4f9f6bd7
parent 55140 7eb0c04e4c40
child 55142 378ae9e46175
prefer self-contained user-space tool;
src/Pure/Isar/calculation.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Pure.thy
src/Pure/ROOT
src/Pure/ROOT.ML
     1.1 --- a/src/Pure/Isar/calculation.ML	Sat Jan 25 18:18:03 2014 +0100
     1.2 +++ b/src/Pure/Isar/calculation.ML	Sat Jan 25 18:34:05 2014 +0100
     1.3 @@ -95,11 +95,11 @@
     1.4  (* concrete syntax *)
     1.5  
     1.6  val _ = Theory.setup
     1.7 - (Attrib.setup (Binding.name "trans") (Attrib.add_del trans_add trans_del)
     1.8 + (Attrib.setup @{binding trans} (Attrib.add_del trans_add trans_del)
     1.9      "declaration of transitivity rule" #>
    1.10 -  Attrib.setup (Binding.name "sym") (Attrib.add_del sym_add sym_del)
    1.11 +  Attrib.setup @{binding sym} (Attrib.add_del sym_add sym_del)
    1.12      "declaration of symmetry rule" #>
    1.13 -  Attrib.setup (Binding.name "symmetric") (Scan.succeed symmetric)
    1.14 +  Attrib.setup @{binding symmetric} (Scan.succeed symmetric)
    1.15      "resolution with symmetry rule" #>
    1.16    Global_Theory.add_thms
    1.17     [((Binding.empty, transitive_thm), [trans_add]),
    1.18 @@ -197,4 +197,32 @@
    1.19  val moreover = collect false;
    1.20  val ultimately = collect true;
    1.21  
    1.22 +
    1.23 +(* outer syntax *)
    1.24 +
    1.25 +val calc_args =
    1.26 +  Scan.option (@{keyword "("} |-- Parse.!!! ((Parse_Spec.xthms1 --| @{keyword ")"})));
    1.27 +
    1.28 +val _ =
    1.29 +  Outer_Syntax.command @{command_spec "also"} "combine calculation and current facts"
    1.30 +    (calc_args >> (Toplevel.proofs' o also_cmd));
    1.31 +
    1.32 +val _ =
    1.33 +  Outer_Syntax.command @{command_spec "finally"}
    1.34 +    "combine calculation and current facts, exhibit result"
    1.35 +    (calc_args >> (Toplevel.proofs' o finally_cmd));
    1.36 +
    1.37 +val _ =
    1.38 +  Outer_Syntax.command @{command_spec "moreover"} "augment calculation by current facts"
    1.39 +    (Scan.succeed (Toplevel.proof' moreover));
    1.40 +
    1.41 +val _ =
    1.42 +  Outer_Syntax.command @{command_spec "ultimately"}
    1.43 +    "augment calculation by current facts, exhibit result"
    1.44 +    (Scan.succeed (Toplevel.proof' ultimately));
    1.45 +
    1.46 +val _ =
    1.47 +  Outer_Syntax.improper_command @{command_spec "print_trans_rules"} "print transitivity rules"
    1.48 +    (Scan.succeed (Toplevel.unknown_context o Toplevel.keep (print_rules o Toplevel.context_of)));
    1.49 +
    1.50  end;
     2.1 --- a/src/Pure/Isar/isar_syn.ML	Sat Jan 25 18:18:03 2014 +0100
     2.2 +++ b/src/Pure/Isar/isar_syn.ML	Sat Jan 25 18:34:05 2014 +0100
     2.3 @@ -688,30 +688,6 @@
     2.4        Toplevel.skip_proof (fn i => i + 1)));
     2.5  
     2.6  
     2.7 -(* calculational proof commands *)
     2.8 -
     2.9 -val calc_args =
    2.10 -  Scan.option (@{keyword "("} |-- Parse.!!! ((Parse_Spec.xthms1 --| @{keyword ")"})));
    2.11 -
    2.12 -val _ =
    2.13 -  Outer_Syntax.command @{command_spec "also"} "combine calculation and current facts"
    2.14 -    (calc_args >> (Toplevel.proofs' o Calculation.also_cmd));
    2.15 -
    2.16 -val _ =
    2.17 -  Outer_Syntax.command @{command_spec "finally"}
    2.18 -    "combine calculation and current facts, exhibit result"
    2.19 -    (calc_args >> (Toplevel.proofs' o Calculation.finally_cmd));
    2.20 -
    2.21 -val _ =
    2.22 -  Outer_Syntax.command @{command_spec "moreover"} "augment calculation by current facts"
    2.23 -    (Scan.succeed (Toplevel.proof' Calculation.moreover));
    2.24 -
    2.25 -val _ =
    2.26 -  Outer_Syntax.command @{command_spec "ultimately"}
    2.27 -    "augment calculation by current facts, exhibit result"
    2.28 -    (Scan.succeed (Toplevel.proof' Calculation.ultimately));
    2.29 -
    2.30 -
    2.31  (* proof navigation *)
    2.32  
    2.33  val _ =
    2.34 @@ -847,11 +823,6 @@
    2.35        Toplevel.keep (Context_Rules.print_rules o Toplevel.context_of)));
    2.36  
    2.37  val _ =
    2.38 -  Outer_Syntax.improper_command @{command_spec "print_trans_rules"} "print transitivity rules"
    2.39 -    (Scan.succeed (Toplevel.unknown_context o
    2.40 -      Toplevel.keep (Calculation.print_rules o Toplevel.context_of)));
    2.41 -
    2.42 -val _ =
    2.43    Outer_Syntax.improper_command @{command_spec "print_methods"} "print methods of this theory"
    2.44      (Scan.succeed (Toplevel.unknown_theory o
    2.45        Toplevel.keep (Method.print_methods o Toplevel.theory_of)));
     3.1 --- a/src/Pure/Pure.thy	Sat Jan 25 18:18:03 2014 +0100
     3.2 +++ b/src/Pure/Pure.thy	Sat Jan 25 18:34:05 2014 +0100
     3.3 @@ -103,6 +103,7 @@
     3.4  begin
     3.5  
     3.6  ML_file "Isar/isar_syn.ML"
     3.7 +ML_file "Isar/calculation.ML"
     3.8  ML_file "Tools/rail.ML"
     3.9  ML_file "Tools/rule_insts.ML";
    3.10  ML_file "Tools/find_theorems.ML"
     4.1 --- a/src/Pure/ROOT	Sat Jan 25 18:18:03 2014 +0100
     4.2 +++ b/src/Pure/ROOT	Sat Jan 25 18:34:05 2014 +0100
     4.3 @@ -106,7 +106,6 @@
     4.4      "Isar/attrib.ML"
     4.5      "Isar/auto_bind.ML"
     4.6      "Isar/bundle.ML"
     4.7 -    "Isar/calculation.ML"
     4.8      "Isar/class.ML"
     4.9      "Isar/class_declaration.ML"
    4.10      "Isar/code.ML"
     5.1 --- a/src/Pure/ROOT.ML	Sat Jan 25 18:18:03 2014 +0100
     5.2 +++ b/src/Pure/ROOT.ML	Sat Jan 25 18:34:05 2014 +0100
     5.3 @@ -236,9 +236,6 @@
     5.4  use "Isar/method.ML";
     5.5  use "Isar/proof.ML";
     5.6  use "Isar/element.ML";
     5.7 -
     5.8 -(*derived theory and proof elements*)
     5.9 -use "Isar/calculation.ML";
    5.10  use "Isar/obtain.ML";
    5.11  
    5.12  (*local theories and targets*)