Mercurial Mercurial > wneuper > isa / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
src/Tools/isac/MathEngBasic/ctree-basic-TEST.sml
changeset 60771 1b072aab8f4e
parent 60704 af9ec1fc81b4 
     1.1 --- a/src/Tools/isac/MathEngBasic/ctree-basic-TEST.sml	Fri Dec 01 05:51:18 2023 +0100
     1.2 +++ b/src/Tools/isac/MathEngBasic/ctree-basic-TEST.sml	Fri Dec 01 06:08:22 2023 +0100
     1.3 @@ -7,7 +7,7 @@
     1.4            BASIC_CALC_TREE
     1.5  *)
     1.6  
     1.7 -signature BASIC_CALC_TREE_TEST =
     1.8 +signature BASIC_CALC_TREE_POS =
     1.9  sig
    1.10  (**** signature ****)
    1.11  (** the basic datatype **)
    1.12 @@ -46,8 +46,8 @@
    1.13    val g_spec : ppobj -> References_Def.T
    1.14    val g_loc : ppobj -> (Istate_Def.T * Proof.context) option * (Istate_Def.T * Proof.context) option
    1.15    val g_form : ppobj -> term
    1.16 -  val g_pbl : ppobj -> Model_Def.i_model_TEST
    1.17 -  val g_met : ppobj -> Model_Def.i_model_TEST
    1.18 +  val g_pbl : ppobj -> Model_Def.i_model_POS
    1.19 +  val g_met : ppobj -> Model_Def.i_model_POS
    1.20    val g_metID : ppobj -> MethodC.id
    1.21    val g_result : ppobj -> Celem.result
    1.22    val g_tac : ppobj -> Tactic.input
    1.23 @@ -106,7 +106,7 @@
    1.24  end
    1.25  
    1.26  (**)
    1.27 -structure CTbasic_TEST(**): BASIC_CALC_TREE_TEST(**) =
    1.28 +structure CTbasic_POS(**): BASIC_CALC_TREE_POS(**) =
    1.29  struct
    1.30  (**)
    1.31  open Pos
    1.32 @@ -181,8 +181,8 @@
    1.33  	           References_Def.T *  (* updated by Refine_Tacitly                                  *)
    1.34  	           term,            (* headline of calc-head, as calculated initially(!)             *)
    1.35      spec  : References_Def.T, (* explicitly input                                              *)
    1.36 -    probl : Model_Def.i_model_TEST,(* = I_Model.T for interactive input to a Problem                *)
    1.37 -    meth  : Model_Def.i_model_TEST,(* = I_Model.T for interactive input to a MethodC                *)
    1.38 +    probl : Model_Def.i_model_POS,(* = I_Model.T for interactive input to a Problem                *)
    1.39 +    meth  : Model_Def.i_model_POS,(* = I_Model.T for interactive input to a MethodC                *)
    1.40      ctxt  : Proof.context,    (* used while specifying this (Sub-)Problem and MethodC          *)
    1.41      loc   : (Istate_Def.T * Proof.context) option  (* like in PrfObj, calling this SubProblem  *)
    1.42            * (Istate_Def.T * Proof.context) option, (* like in PrfObj, finishing the SubProblem *)
wneuper/isa