1.1 --- a/src/Tools/isac/MathEngBasic/ctree-basic.sml	Fri May 08 11:00:07 2020 +0200
     1.2 +++ b/src/Tools/isac/MathEngBasic/ctree-basic.sml	Fri May 08 11:01:11 2020 +0200
     1.3 @@ -199,18 +199,18 @@
     1.4              (Istate_Def.T *   (* script interpreter state                                      *)
     1.5               Proof.context)   (* context for provers, type inference                           *)
     1.6              option,           (* both for interpreter location on Res                          *)
     1.7 -                              (*(NONE,NONE) <==> empty ! see update_loc, get_loc            *)
     1.8 +                              (* (NONE,NONE) <==> empty ! see update_loc, get_loc              *)
     1.9  	  branch: branch,           (* only rudimentary                                              *)
    1.10  	  result: Celem.result,     (* result and assumptions                                        *)
    1.11  	  ostate: ostate}           (* Complete <=> result is OK                                     *)
    1.12  | PblObj of                   (* a step serving a whole specification-phase                    *)
    1.13 -   {fmz   : Model_Def.form_T,        (* from init:FIXME never use this spec;-drop                     *)
    1.14 -    origin: (Model_Def.o_model) *(* from fmz+pbt+met for efficiently adding items to probl, meth  *)
    1.15 -	           Spec.T *     (* updated by Refine_Tacitly                                     *)
    1.16 +   {fmz   : Model_Def.form_T, (* from init:FIXME never use this spec;-drop                     *)
    1.17 +    origin: (Model_Def.o_model) *(* = O_Model.T for efficiently checking input to I_Model      *)
    1.18 +	           Spec.T *         (* updated by Refine_Tacitly                                     *)
    1.19  	           term,            (* headline of calc-head, as calculated initially(!)             *)
    1.20 -    spec  : Spec.T,       (* explicitly input                                              *)
    1.21 -    probl : Model_Def.i_model,   (* itms explicitly input                                         *)
    1.22 -    meth  : Model_Def.i_model,   (* itms automatically added to copy of probl                     *)
    1.23 +    spec  : Spec.T,           (* explicitly input                                              *)
    1.24 +    probl : Model_Def.i_model,(* = I_Model.T for interactive input to a Problem                *)
    1.25 +    meth  : Model_Def.i_model,(* = I_Model.T for interactive input to a Method                 *)
    1.26      ctxt  : Proof.context,    (* used while specifying this (Sub-)Problem and Method           *)
    1.27      loc   : (Istate_Def.T * Proof.context) option  (* like in PrfObj, calling this SubProblem  *)
    1.28            * (Istate_Def.T * Proof.context) option, (* like in PrfObj, finishing the SubProblem *)

     2.1 --- a/src/Tools/isac/Specify/Input_Descript.thy	Fri May 08 11:00:07 2020 +0200
     2.2 +++ b/src/Tools/isac/Specify/Input_Descript.thy	Fri May 08 11:01:11 2020 +0200
     2.3 @@ -10,7 +10,7 @@
     2.4  theory Input_Descript imports "~~/src/Tools/isac/BaseDefinitions/BaseDefinitions"
     2.5  begin
     2.6  
     2.7 -subsection \<open>typedecl for descriptions of input in specify-phase\<close>
     2.8 +subsection \<open>typedecl for descriptors of input in specify-phase\<close>
     2.9  text \<open>
    2.10    The typedecl below MUST ALL be registered in "fun is_dsc"
    2.11  \<close>
    2.12 @@ -24,7 +24,7 @@
    2.13    typedecl unknow  (* input without dsc in fmz=[]                                 *)
    2.14    typedecl cpy     (* copy-named variables identified by .._0, .._i .._' in pbt   *)
    2.15  
    2.16 -subsection \<open>consts for general descriptions of input in specify-phase\<close>
    2.17 +subsection \<open>consts for general descriptors of input in the specify-phase\<close>
    2.18  
    2.19  consts
    2.20  (*TODO.180331: review for localisation of model-patterns and of method's guards*)