src/Tools/isac/MathEngBasic/tactic.sml
changeset 59740 5b8b3475d5a6
parent 59737 5e2834f8a655
child 59741 e2a808ba0467
     1.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml	Tue Dec 17 16:35:29 2019 +0100
     1.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml	Tue Dec 17 17:19:34 2019 +0100
     1.3 @@ -9,98 +9,10 @@
     1.4  *)
     1.5  signature TACTIC =
     1.6  sig
     1.7 -  datatype T =
     1.8 -    Add_Find' of Rule.cterm' * Model.itm list | Add_Given' of Rule.cterm' * Model.itm list 
     1.9 -  | Add_Relation' of Rule.cterm' * Model.itm list
    1.10 -  | Apply_Assumption' of term list * term
    1.11 -  | Apply_Method' of Celem.metID * term option * Istate_Def.T * Proof.context
    1.12 -
    1.13 -  | Begin_Sequ' | Begin_Trans' of term
    1.14 -  | Split_And' of term | Split_Or' of term | Split_Intersect' of term
    1.15 -  | Conclude_And' of term | Conclude_Or' of term | Collect_Trues' of term
    1.16 -  | End_Sequ' | End_Trans' of Selem.result
    1.17 -  | End_Ruleset' of term | End_Subproblem' of term | End_Intersect' of term | End_Proof''
    1.18 -
    1.19 -  | CAScmd' of term
    1.20 -  | Calculate' of Rule.theory' * string * term * (term * Celem.thm')
    1.21 -  | Check_Postcond' of Celem.pblID * Selem.result
    1.22 -  | Check_elementwise' of term * Rule.cterm' * Selem.result
    1.23 -  | Del_Find' of Rule.cterm' | Del_Given' of Rule.cterm' | Del_Relation' of Rule.cterm'
    1.24 -
    1.25 -  | Derive' of Rule.rls
    1.26 -  | Detail_Set' of Rule.theory' * bool * Rule.rls * term * Selem.result
    1.27 -  | Detail_Set_Inst' of Rule.theory' * bool * Rule.subst * Rule.rls * term * Selem.result
    1.28 -  | End_Detail' of Selem.result
    1.29 -
    1.30 -  | Empty_Tac_
    1.31 -  | Free_Solve'
    1.32 -
    1.33 -  | Init_Proof' of Rule.cterm' list * Celem.spec
    1.34 -  | Model_Problem' of Celem.pblID * Model.itm list * Model.itm list
    1.35 -  | Or_to_List' of term * term
    1.36 -  | Refine_Problem' of Celem.pblID * (Model.itm list * (bool * term) list)
    1.37 -  | Refine_Tacitly' of Celem.pblID * Celem.pblID * Rule.domID * Celem.metID * Model.itm list
    1.38 -
    1.39 -  | Rewrite' of Rule.theory' * Rule.rew_ord' * Rule.rls * bool * Celem.thm'' * term * Selem.result
    1.40 -  | Rewrite_Asm' of Rule.theory' * Rule.rew_ord' * Rule.rls * bool * Celem.thm'' * term * Selem.result
    1.41 -  | Rewrite_Inst' of Rule.theory' * Rule.rew_ord' * Rule.rls * bool * Rule.subst * Celem.thm'' * term * Selem.result
    1.42 -  | Rewrite_Set' of Rule.theory' * bool * Rule.rls * term * Selem.result
    1.43 -  | Rewrite_Set_Inst' of Rule.theory' * bool * Rule.subst * Rule.rls * term * Selem.result
    1.44 -
    1.45 -  | Specify_Method' of Celem.metID * Model.ori list * Model.itm list
    1.46 -  | Specify_Problem' of Celem.pblID * (bool * (Model.itm list * (bool * term) list))
    1.47 -  | Specify_Theory' of Rule.domID
    1.48 -  | Subproblem' of Celem.spec * Model.ori list * term * Selem.fmz_ * Proof.context * term
    1.49 -  | Substitute' of Rule.rew_ord_ * Rule.rls * Selem.subte * term * term
    1.50 -  | Tac_ of theory * string * string * string
    1.51 -  | Take' of term | Take_Inst' of term
    1.52 +  datatype T = datatype Tactic_Def.T
    1.53    val string_of : T -> string
    1.54  
    1.55 -  datatype input =
    1.56 -    Add_Find of Rule.cterm' | Add_Given of Rule.cterm' | Add_Relation of Rule.cterm'
    1.57 -  | Apply_Assumption of Rule.cterm' list
    1.58 -  | Apply_Method of Celem.metID
    1.59 -  (*/--- TODO: re-design ? -----------------------------------------------------------------\*)
    1.60 -  | Begin_Sequ | Begin_Trans
    1.61 -  | Split_And | Split_Or | Split_Intersect
    1.62 -  | Conclude_And | Conclude_Or | Collect_Trues
    1.63 -  | End_Sequ | End_Trans
    1.64 -  | End_Ruleset | End_Subproblem | End_Intersect | End_Proof'
    1.65 -  (*\--- TODO: re-design ? -----------------------------------------------------------------/*)
    1.66 -  | CAScmd of Rule.cterm'
    1.67 -  | Calculate of string
    1.68 -  | Check_Postcond of Celem.pblID
    1.69 -  | Check_elementwise of Rule.cterm'
    1.70 -  | Del_Find of Rule.cterm' | Del_Given of Rule.cterm' | Del_Relation of Rule.cterm'
    1.71 -
    1.72 -  | Derive of Rule.rls'
    1.73 -  | Detail_Set of Rule.rls'
    1.74 -  | Detail_Set_Inst of Selem.subs * Rule.rls'
    1.75 -  | End_Detail
    1.76 -
    1.77 -  | Empty_Tac
    1.78 -  | Free_Solve
    1.79 -
    1.80 -  | Init_Proof of Rule.cterm' list * Celem.spec
    1.81 -  | Model_Problem
    1.82 -  | Or_to_List
    1.83 -  | Refine_Problem of Celem.pblID
    1.84 -  | Refine_Tacitly of Celem.pblID
    1.85 -
    1.86 -  | Rewrite of Celem.thm''
    1.87 -  | Rewrite_Asm of Celem.thm''
    1.88 -  | Rewrite_Inst of Selem.subs * Celem.thm''
    1.89 -  | Rewrite_Set of Rule.rls'
    1.90 -  | Rewrite_Set_Inst of Selem.subs * Rule.rls'
    1.91 -
    1.92 -  | Specify_Method of Celem.metID
    1.93 -  | Specify_Problem of Celem.pblID
    1.94 -  | Specify_Theory of Rule.domID
    1.95 -  | Subproblem of Rule.domID * Celem.pblID
    1.96 -
    1.97 -  | Substitute of Selem.sube
    1.98 -  | Tac of string
    1.99 -  | Take of Rule.cterm' | Take_Inst of Rule.cterm'
   1.100 +  datatype input = datatype Tactic_Def.input
   1.101    val tac2str : input -> string
   1.102  
   1.103    val eq_tac : input * input -> bool
   1.104 @@ -138,112 +50,11 @@
   1.105         initacs start with a formula different from the preceding formula.
   1.106     see 'type tac_' for the internal representation of tactics
   1.107  *)
   1.108 -datatype input =
   1.109 -    Add_Find of Rule.cterm' | Add_Given of Rule.cterm' | Add_Relation of Rule.cterm'
   1.110 -  | Apply_Assumption of Rule.cterm' list
   1.111 -  | Apply_Method of Celem.metID
   1.112 -    (* creates an "istate" in PblObj.env; in case of "init_form" 
   1.113 -      creates a formula at ((lev_on o lev_dn) p, Frm) and in this "ppobj.loc"
   1.114 -      a "SOME istate" at fst of "loc".
   1.115 -      As each step (in the solve-phase) has a resulting formula (at the front-end)
   1.116 -      Apply_Method also does the 1st step in the script (an "initac") if there is no "init_form" *)  
   1.117 -  (*/--- TODO: re-design ? -----------------------------------------------------------------\*)
   1.118 -  | Begin_Sequ | Begin_Trans
   1.119 -  | Split_And | Split_Or | Split_Intersect
   1.120 -  | Conclude_And | Conclude_Or | Collect_Trues
   1.121 -  | End_Sequ | End_Trans
   1.122 -  | End_Ruleset | End_Subproblem (* WN0509 drop *) | End_Intersect | End_Proof'
   1.123 -  (*\--- TODO: re-design ? -----------------------------------------------------------------/*)
   1.124 -  | CAScmd of Rule.cterm'
   1.125 -  | Calculate of string
   1.126 -  | Check_Postcond of Celem.pblID
   1.127 -  | Check_elementwise of Rule.cterm'
   1.128 -  | Del_Find of Rule.cterm' | Del_Given of Rule.cterm' | Del_Relation of Rule.cterm'
   1.129 +datatype input = datatype Tactic_Def.input
   1.130  
   1.131 -  | Derive of Rule.rls'                 (* WN0509 drop *)
   1.132 -  | Detail_Set of Rule.rls'             (* WN0509 drop *)
   1.133 -  | Detail_Set_Inst of Selem.subs * Rule.rls' (* WN0509 drop *)
   1.134 -  | End_Detail                     (* WN0509 drop *)
   1.135 +val tac2str = Tactic_Def.tac2str
   1.136  
   1.137 -  | Empty_Tac
   1.138 -  | Free_Solve
   1.139 -
   1.140 -  | Init_Proof of Rule.cterm' list * Celem.spec
   1.141 -  | Model_Problem
   1.142 -  | Or_to_List
   1.143 -  | Refine_Problem of Celem.pblID
   1.144 -  | Refine_Tacitly of Celem.pblID
   1.145 -
   1.146 -   (* rewrite-tactics can transport a (thmID, thm) to and (!) from the java-front-end
   1.147 -     because there all the thms are present with both (thmID, thm)
   1.148 -     (where user-views can show both or only one of (thmID, thm)),
   1.149 -     and thm is created from ThmID by assoc_thm'' when entering isabisac *)
   1.150 -  | Rewrite of Celem.thm''
   1.151 -  | Rewrite_Asm of Celem.thm''
   1.152 -  | Rewrite_Inst of Selem.subs * Celem.thm''
   1.153 -  | Rewrite_Set of Rule.rls'
   1.154 -  | Rewrite_Set_Inst of Selem.subs * Rule.rls'
   1.155 -
   1.156 -  | Specify_Method of Celem.metID
   1.157 -  | Specify_Problem of Celem.pblID
   1.158 -  | Specify_Theory of Rule.domID
   1.159 -  | Subproblem of Rule.domID * Celem.pblID (* WN0509 drop *)
   1.160 -
   1.161 -  | Substitute of Selem.sube
   1.162 -  | Tac of string               (* WN0509 drop *)
   1.163 -  | Take of Rule.cterm' | Take_Inst of Rule.cterm'
   1.164 -
   1.165 -fun tac2str ma = case ma of
   1.166 -    Init_Proof (ppc, spec)  => 
   1.167 -      "Init_Proof "^(pair2str (strs2str ppc, Celem.spec2str spec))
   1.168 -  | Model_Problem           => "Model_Problem "
   1.169 -  | Refine_Tacitly pblID    => "Refine_Tacitly " ^ strs2str pblID 
   1.170 -  | Refine_Problem pblID    => "Refine_Problem " ^ strs2str pblID 
   1.171 -  | Add_Given cterm'        => "Add_Given " ^ cterm'
   1.172 -  | Del_Given cterm'        => "Del_Given " ^ cterm'
   1.173 -  | Add_Find cterm'         => "Add_Find " ^ cterm'
   1.174 -  | Del_Find cterm'         => "Del_Find " ^ cterm'
   1.175 -  | Add_Relation cterm'     => "Add_Relation " ^ cterm'
   1.176 -  | Del_Relation cterm'     => "Del_Relation " ^ cterm'
   1.177 -
   1.178 -  | Specify_Theory domID    => "Specify_Theory " ^ quote domID
   1.179 -  | Specify_Problem pblID   => "Specify_Problem " ^ strs2str pblID
   1.180 -  | Specify_Method metID    => "Specify_Method " ^ strs2str metID
   1.181 -  | Apply_Method metID      => "Apply_Method " ^ strs2str metID
   1.182 -  | Check_Postcond pblID    => "Check_Postcond " ^ strs2str pblID
   1.183 -  | Free_Solve              => "Free_Solve"
   1.184 -
   1.185 -  | Rewrite_Inst (subs, (id, thm)) =>
   1.186 -    "Rewrite_Inst " ^ (pair2str (subs2str subs, spair2str (id, thm |> Thm.prop_of |> Rule.term2str)))
   1.187 -  | Rewrite (id, thm) => "Rewrite " ^ spair2str (id, thm |> Thm.prop_of |> Rule.term2str)
   1.188 -  | Rewrite_Asm (id, thm) => "Rewrite_Asm " ^ spair2str (id, thm |> Thm.prop_of |> Rule.term2str)
   1.189 -  | Rewrite_Set_Inst (subs, rls) => 
   1.190 -    "Rewrite_Set_Inst " ^ pair2str (subs2str subs, quote rls)
   1.191 -  | Rewrite_Set rls         => "Rewrite_Set " ^ quote rls
   1.192 -  | Detail_Set rls          => "Detail_Set " ^ quote rls
   1.193 -  | Detail_Set_Inst (subs, rls) =>  "Detail_Set_Inst " ^ pair2str (subs2str subs, quote rls)
   1.194 -  | End_Detail              => "End_Detail"
   1.195 -  | Derive rls'             => "Derive " ^ rls' 
   1.196 -  | Calculate op_           => "Calculate " ^ op_ 
   1.197 -  | Substitute sube         => "Substitute " ^ Selem.sube2str sube	     
   1.198 -  | Apply_Assumption ct's   => "Apply_Assumption " ^ strs2str ct's
   1.199 -
   1.200 -  | Take cterm'             => "Take " ^ quote cterm'
   1.201 -  | Take_Inst cterm'        => "Take_Inst " ^ quote cterm'
   1.202 -  | Subproblem (domID, pblID) => "Subproblem " ^ pair2str (domID, strs2str pblID)
   1.203 -  | End_Subproblem          => "End_Subproblem"
   1.204 -  | CAScmd cterm'           => "CAScmd " ^ quote cterm'
   1.205 -
   1.206 -  | Check_elementwise cterm'=> "Check_elementwise " ^ quote cterm'
   1.207 -  | Or_to_List              => "Or_to_List "
   1.208 -  | Collect_Trues           => "Collect_Trues"
   1.209 -
   1.210 -  | Empty_Tac               => "Empty_Tac"
   1.211 -  | Tac string              => "Tac " ^ string
   1.212 -  | End_Proof'              => "input End_Proof'"
   1.213 -  | _                       => "tac2str not impl. for ?!";
   1.214 -
   1.215 -fun is_empty_tac input = case input of Empty_Tac => true | _ => false
   1.216 +val is_empty_tac = Tactic_Def.is_empty_tac
   1.217  
   1.218  fun eq_tac (Rewrite (id1, _), Rewrite (id2, _)) = id1 = id2
   1.219    | eq_tac (Rewrite_Inst (_, (id1, _)), Rewrite_Inst (_, (id2, _))) = id1 = id2
   1.220 @@ -331,126 +142,9 @@
   1.221    and re-calculate result if t<>t'
   1.222    TODO.WN161219: replace *every* cterm' by term
   1.223  *)
   1.224 -  datatype T =
   1.225 -    Add_Find' of Rule.cterm' * Model.itm list | Add_Given' of Rule.cterm' * Model.itm list 
   1.226 -  | Add_Relation' of Rule.cterm' * Model.itm list
   1.227 -  | Apply_Assumption' of term list * term
   1.228 -  | Apply_Method' of Celem.metID * term option * Istate_Def.T * Proof.context
   1.229 -  (*/--- TODO: re-design ? -----------------------------------------------------------------\*)
   1.230 -  | Begin_Sequ' | Begin_Trans' of term
   1.231 -  | Split_And' of term | Split_Or' of term | Split_Intersect' of term
   1.232 -  | Conclude_And' of term | Conclude_Or' of term | Collect_Trues' of term
   1.233 -  | End_Sequ' | End_Trans' of Selem.result
   1.234 -  | End_Ruleset' of term | End_Subproblem' of term | End_Intersect' of term | End_Proof''
   1.235 -  (*\--- TODO: re-design ? -----------------------------------------------------------------/*)
   1.236 -  | CAScmd' of term
   1.237 -  | Calculate' of Rule.theory' * string * term * (term * Celem.thm')
   1.238 -  | Check_Postcond' of Celem.pblID *
   1.239 -    Selem.result (* returnvalue of script in solve *)
   1.240 -  | Check_elementwise' of (*special case:*)
   1.241 -    term *       (* (1) the current formula: [x=1,x=...]     *)
   1.242 -    string *     (* (2) the pred from Check_elementwise      *)
   1.243 -    Selem.result (* (3) composed from (1) and (2): {x. pred} *)
   1.244 -  | Del_Find' of Rule.cterm' | Del_Given' of Rule.cterm' | Del_Relation' of Rule.cterm'
   1.245 +  datatype T = datatype Tactic_Def.T
   1.246  
   1.247 -  | Derive' of Rule.rls
   1.248 -  | Detail_Set' of Rule.theory' * bool * Rule.rls * term * Selem.result
   1.249 -  | Detail_Set_Inst' of Rule.theory' * bool * Rule.subst * Rule.rls * term * Selem.result
   1.250 -  | End_Detail' of Selem.result
   1.251 -
   1.252 -  | Empty_Tac_
   1.253 -  | Free_Solve'
   1.254 -
   1.255 -  | Init_Proof' of Rule.cterm' list * Celem.spec
   1.256 -  | Model_Problem' of Celem.pblID * 
   1.257 -    Model.itm list *  (* the 'untouched' pbl        *)
   1.258 -    Model.itm list    (* the casually completed met *)
   1.259 -  | Or_to_List' of term * term
   1.260 -  | Refine_Problem' of Celem.pblID * (Model.itm list * (bool * term) list)
   1.261 -  | Refine_Tacitly' of
   1.262 -    Celem.pblID *     (* input*)
   1.263 -    Celem.pblID *     (* the refined from applicable_in                                       *)
   1.264 -    Rule.domID *     (* from new pbt?! filled in specify                                     *)
   1.265 -    Celem.metID *     (* from new pbt?! filled in specify                                     *)
   1.266 -    Model.itm list    (* drop ! 9.03: remains [] for Model_Problem recognizing its activation *)
   1.267 -  | Rewrite' of Rule.theory' * Rule.rew_ord' * Rule.rls * bool * Celem.thm'' * term * Selem.result
   1.268 -  | Rewrite_Asm' of Rule.theory' * Rule.rew_ord' * Rule.rls * bool * Celem.thm'' * term * Selem.result
   1.269 -  | Rewrite_Inst' of Rule.theory' * Rule.rew_ord' * Rule.rls * bool * Rule.subst * Celem.thm'' * term * Selem.result
   1.270 -  | Rewrite_Set' of Rule.theory' * bool * Rule.rls * term * Selem.result
   1.271 -  | Rewrite_Set_Inst' of Rule.theory' * bool * Rule.subst * Rule.rls * term * Selem.result
   1.272 -
   1.273 -  | Specify_Method' of Celem.metID * Model.ori list * Model.itm list
   1.274 -  | Specify_Problem' of Celem.pblID * 
   1.275 -    (bool *                  (* matches	                                  *)
   1.276 -      (Model.itm list *      (* ppc	                                      *)
   1.277 -        (bool * term) list)) (* preconditions                             *)
   1.278 -  | Specify_Theory' of Rule.domID
   1.279 -  | Subproblem' of
   1.280 -    Celem.spec * 
   1.281 -		(Model.ori list) *       (* filled in associate Subproblem'           *)
   1.282 -		term *                   (* filled -"-, headline of calc-head         *)
   1.283 -		Selem.fmz_ *             
   1.284 -    Proof.context *          (* DEPRECATED shifted into loc for all ppobj *)
   1.285 -		term                     (* Subproblem (thyID, pbl) OR cascmd         *)  
   1.286 -  | Substitute' of           
   1.287 -    Rule.rew_ord_ *          (* for re-calculation                        *)
   1.288 -    Rule.rls *               (* for re-calculation                        *)
   1.289 -    Selem.subte *            (* the 'substitution': terms of type bool    *)
   1.290 -    term *                   (* to be substituted into                    *)
   1.291 -    term                     (* resulting from the substitution           *)
   1.292 -  | Tac_ of theory * string * string * string
   1.293 -  | Take' of term | Take_Inst' of term
   1.294 -
   1.295 -fun string_of ma = case ma of
   1.296 -    Init_Proof' (ppc, spec)  => "Init_Proof' " ^ pair2str (strs2str ppc, Celem.spec2str spec)
   1.297 -  | Model_Problem' (pblID, _, _) => "Model_Problem' " ^ strs2str pblID
   1.298 -  | Refine_Tacitly'(p, prefin, domID, metID, _) => "Refine_Tacitly' (" ^ strs2str p ^ ", " ^
   1.299 -    strs2str prefin ^ ", " ^ domID ^ ", " ^ strs2str metID ^ ", pbl-itms)"
   1.300 -  | Refine_Problem' _ => "Refine_Problem' (" ^ (*matchs2str ms*)"..." ^ ")"
   1.301 -  | Add_Given' _ => "Add_Given' "(*^cterm'*)
   1.302 -  | Del_Given' _ => "Del_Given' "(*^cterm'*)
   1.303 -  | Add_Find' _ => "Add_Find' "(*^cterm'*)
   1.304 -  | Del_Find' _ => "Del_Find' "(*^cterm'*)
   1.305 -  | Add_Relation' _ => "Add_Relation' "(*^cterm'*)
   1.306 -  | Del_Relation' _ => "Del_Relation' "(*^cterm'*)
   1.307 -
   1.308 -  | Specify_Theory' domID => "Specify_Theory' " ^ quote domID
   1.309 -  | Specify_Problem' (pI, (ok, _)) =>  "Specify_Problem' " ^ 
   1.310 -    spair2str (strs2str pI, spair2str (bool2str ok, spair2str ("itms2str_ itms", "items2str pre")))
   1.311 -  | Specify_Method' (pI, oris, _) => "Specify_Method' (" ^ 
   1.312 -    Celem.metID2str pI ^ ", " ^ Model.oris2str oris ^ ", )"
   1.313 -
   1.314 -  | Apply_Method' (metID, _, _, _) => "Apply_Method' " ^ strs2str metID
   1.315 -  | Check_Postcond' (pblID, (scval, asm)) => "Check_Postcond' " ^
   1.316 -      (spair2str (strs2str pblID, spair2str (Rule.term2str scval, Rule.terms2str asm)))
   1.317 -
   1.318 -  | Free_Solve' => "Free_Solve'"
   1.319 -
   1.320 -  | Rewrite_Inst' (*subs,thm'*) _ => "Rewrite_Inst' "(*^(pair2str (subs2str subs, spair2str thm'))*)
   1.321 -  | Rewrite' _(*thm'*) => "Rewrite' "(*^(spair2str thm')*)
   1.322 -  | Rewrite_Asm' _(*thm'*) => "Rewrite_Asm' "(*^(spair2str thm')*)
   1.323 -  | Rewrite_Set_Inst' _(*subs,thm'*) => "Rewrite_Set_Inst' "(*^(pair2str (subs2str subs, quote rls))*)
   1.324 -  | Rewrite_Set' (thy', pasm, rls', f, (f', asm)) => "Rewrite_Set' (" ^ thy' ^ "," ^ bool2str pasm ^
   1.325 -    "," ^ Rule.id_rls rls' ^ "," ^ Rule.term2str f ^ ",(" ^ Rule.term2str f' ^ "," ^ Rule.terms2str asm ^ "))"
   1.326 -  | End_Detail' _ => "End_Detail' xxx"
   1.327 -  | Detail_Set' _ => "Detail_Set' xxx"
   1.328 -  | Detail_Set_Inst' _ => "Detail_Set_Inst' xxx"
   1.329 -
   1.330 -  | Derive' rls => "Derive' " ^ Rule.id_rls rls
   1.331 -  | Calculate'  _ => "Calculate' "
   1.332 -  | Substitute' _ => "Substitute' "(*^(subs2str subs)*)    
   1.333 -  | Apply_Assumption' _(* ct's*) => "Apply_Assumption' "(*^(strs2str ct's)*)
   1.334 -
   1.335 -  | Take' _(*cterm'*) => "Take' "(*^(quote cterm'	)*)
   1.336 -  | Take_Inst' _(*cterm'*) => "Take_Inst' "(*^(quote cterm' )*)
   1.337 -  | Subproblem' _(*(spec, oris, _, _, _, pbl_form)*) => 
   1.338 -    "Subproblem' "(*^(pair2str (domID, strs2str ,))*)
   1.339 -  | End_Subproblem' _ => "End_Subproblem'"
   1.340 -  | CAScmd' _(*cterm'*) => "CAScmd' "(*^(quote cterm')*)
   1.341 -
   1.342 -  | Empty_Tac_ => "Empty_Tac_"
   1.343 -  | Tac_ (_, form, id, result) => "Tac_ (thy," ^ form ^ "," ^ id ^ "," ^ result ^ ")"
   1.344 -  | _  => "string_of not impl. for arg";
   1.345 +val string_of = Tactic_Def.string_of
   1.346  
   1.347  fun input_from_T (Refine_Tacitly' (pI, _, _, _, _)) = Refine_Tacitly pI
   1.348    | input_from_T (Model_Problem' (_, _, _)) = Model_Problem