1.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml Sat May 02 12:13:20 2020 +0200
1.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml Sat May 02 15:41:27 2020 +0200
1.3 @@ -4,7 +4,7 @@
1.4
1.5 regular expression for search:
1.6
1.7 -Add_Find|Add_Given|Add_Relation|Apply_Method|Begin_Sequ|Begin_Trans|Split_And|Split_Or|Split_Intersect|Conclude_And|Conclude_Or|End_Sequ|End_Trans|End_Ruleset|End_Subproblem|End_Intersect|End_Proof|CAScmd|Calculate|Check_Postcond|Check_elementwise|Del_Find|Del_Given|Del_Relation|Derive|Detail_Set|Detail_Set_Inst|End_Detail|Empty_Tac|Free_Solve|Init_Proof|Model_Problem Or_to_List|Refine_Problem|Refine_Tacitly| Rewrite|Rewrite_Inst|Rewrite_Set|Rewrite_Set_Inst|Specify_Method|Specify_Problem|Specify_Theory|Subproblem|Substitute|Tac|Take|Take_Inst
1.8 +Add_Find|Add_Given|Add_Relation|Apply_Method|Begin_Sequ|Begin_Trans|Split_And|Split_Or|Split_Intersect|Conclude_And|Conclude_Or|End_Sequ|End_Trans|End_Ruleset|End_Subproblem|End_Intersect|End_Proof|Calculate|Check_Postcond|Check_elementwise|Del_Find|Del_Given|Del_Relation|Derive|Detail_Set|Detail_Set_Inst|End_Detail|Empty_Tac|Free_Solve|Init_Proof|Model_Problem Or_to_List|Refine_Problem|Refine_Tacitly| Rewrite|Rewrite_Inst|Rewrite_Set|Rewrite_Set_Inst|Specify_Method|Specify_Problem|Specify_Theory|Subproblem|Substitute|Tac|Take|Take_Inst
1.9
1.10 *)
1.11 signature TACTIC =
1.12 @@ -21,7 +21,6 @@
1.13 | Specify_Problem' of Problem.id * (bool * (Model.itm list * (bool * term) list))
1.14 | Specify_Theory' of ThyC.id
1.15 (* ^^^^^--------------------- for specify-phase, for solve-phase ---------------------vvvvv*)
1.16 - | CAScmd' of term
1.17 | Calculate' of ThyC.id * string * term * (term * ThmC.T)
1.18 | Check_Postcond' of Problem.id * term
1.19 | Check_elementwise' of term * TermC.as_string * Selem.result
1.20 @@ -55,7 +54,6 @@
1.21 | Specify_Problem of Problem.id
1.22 | Specify_Theory of ThyC.id
1.23 (* ^^^^^--------------------- for specify-phase, for solve-phase ---------------------vvvvv*)
1.24 - | CAScmd of TermC.as_string
1.25 | Calculate of string
1.26 | Check_Postcond of Problem.id
1.27 | Check_elementwise of TermC.as_string
1.28 @@ -121,7 +119,6 @@
1.29 | Specify_Problem of Problem.id
1.30 | Specify_Theory of ThyC.id
1.31 (* ^^^^^--------------------- for specify-phase, for solve-phase ---------------------vvvvv*)
1.32 - | CAScmd of TermC.as_string
1.33 | Calculate of string
1.34 | Check_Postcond of Problem.id
1.35 | Check_elementwise of TermC.as_string
1.36 @@ -172,7 +169,6 @@
1.37
1.38 | Take cterm' => "Take " ^ quote cterm'
1.39 | Subproblem (domID, pblID) => "Subproblem " ^ pair2str (domID, strs2str pblID)
1.40 - | CAScmd cterm' => "CAScmd " ^ quote cterm'
1.41
1.42 | Check_elementwise cterm'=> "Check_elementwise " ^ quote cterm'
1.43 | Or_to_List => "Or_to_List "
1.44 @@ -210,7 +206,6 @@
1.45
1.46 | Take _ => "Take"
1.47 | Subproblem _ => "Subproblem"
1.48 - | CAScmd _ => "CAScmd"
1.49
1.50 | Check_elementwise _ => "Check_elementwise"
1.51 | Or_to_List => "Or_to_List "
1.52 @@ -324,7 +319,6 @@
1.53 (bool * term) list)) (* individual preconditions marked true/false *)
1.54 | Specify_Theory' of ThyC.id
1.55 (* ^^^^^--------------------- for specify-phase, for solve-phase ---------------------vvvvv*)
1.56 - | CAScmd' of term
1.57 | Calculate' of ThyC.id * string * term * (term * ThmC.T)
1.58 | Check_Postcond' of (* last step in solving a (sub-)Problem *)
1.59 Problem.id * (* id of the Problem to be checked *)
1.60 @@ -399,7 +393,6 @@
1.61 | Take' _(*cterm'*) => "Take' "(*^(quote cterm' )*)
1.62 | Subproblem' _(*(spec, oris, _, _, _, pbl_form)*) =>
1.63 "Subproblem' "(*^(pair2str (domID, strs2str ,))*)
1.64 - | CAScmd' _(*cterm'*) => "CAScmd' "(*^(quote cterm')*)
1.65
1.66 | Empty_Tac_ => "Empty_Tac_"
1.67 | Tac_ (_, form, id, result) => "Tac_ (thy," ^ form ^ "," ^ id ^ "," ^ result ^ ")"