1.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml	Mon May 11 11:38:52 2020 +0200
     1.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml	Mon May 11 12:25:52 2020 +0200
     1.3 @@ -14,10 +14,10 @@
     1.4    | Add_Relation' of TermC.as_string * Model_Def.i_model
     1.5  (*RM*)| Del_Find' of TermC.as_string | Del_Given' of TermC.as_string | Del_Relation' of TermC.as_string
     1.6    | Model_Problem' of Problem.id * Model_Def.i_model * Model_Def.i_model
     1.7 -  | Refine_Problem' of Problem.id * (Model_Def.i_model * (bool * term) list)
     1.8 +  | Refine_Problem' of Problem.id * (Model_Def.i_model * Pre_Conds_Def.T)
     1.9    | Refine_Tacitly' of Problem.id * Problem.id * ThyC.id * Method.id * Model_Def.i_model
    1.10    | Specify_Method' of Method.id * Model_Def.o_model * Model_Def.i_model
    1.11 -  | Specify_Problem' of Problem.id * (bool * (Model_Def.i_model * (bool * term) list))
    1.12 +  | Specify_Problem' of Problem.id * (bool * (Model_Def.i_model * Pre_Conds_Def.T))
    1.13    | Specify_Theory' of ThyC.id
    1.14    (* ^^^^^--------------------- for specify-phase, for solve-phase ---------------------vvvvv*)
    1.15    | Apply_Method' of Method.id * term option * Istate_Def.T * Proof.context
    1.16 @@ -302,7 +302,7 @@
    1.17        Problem.id *     (* id in the Know_Store                               *)
    1.18        Model_Def.i_model * (* the model for the Problem                          *)
    1.19        Model_Def.i_model   (* the model for the method                           *)
    1.20 -  | Refine_Problem' of Problem.id * (Model_Def.i_model * (bool * term) list)
    1.21 +  | Refine_Problem' of Problem.id * (Model_Def.i_model * Pre_Conds_Def.T)
    1.22    | Refine_Tacitly' of                                                      
    1.23        Problem.id *       (* the original id in the Know_Store                *)
    1.24        Problem.id *       (* the id of the refined Problem                    *)
    1.25 @@ -313,7 +313,7 @@
    1.26    | Specify_Problem' of Problem.id * 
    1.27        (bool *                  (* all preconditions evaluate to True         *)
    1.28          (Model_Def.i_model *      (* the model checked for the input id         *)
    1.29 -          (bool * term) list)) (* individual preconditions marked true/false *)
    1.30 +          Pre_Conds_Def.T)) (* individual preconditions marked true/false *)
    1.31    | Specify_Theory' of ThyC.id
    1.32    (* ^^^^^--------------------- for specify-phase, for solve-phase ---------------------vvvvv*)
    1.33    | Apply_Method' of   (* last step in specifu-phse, switch to solve-phase   *)