5 Definitions required for Ctree, renamed later appropriately |
5 Definitions required for Ctree, renamed later appropriately |
6 -------------------------vvvvv + I_Model.T-TEST are the only difference to |
6 -------------------------vvvvv + I_Model.T-TEST are the only difference to |
7 BASIC_CALC_TREE |
7 BASIC_CALC_TREE |
8 *) |
8 *) |
9 |
9 |
10 signature BASIC_CALC_TREE_TEST = |
10 signature BASIC_CALC_TREE_POS = |
11 sig |
11 sig |
12 (**** signature ****) |
12 (**** signature ****) |
13 (** the basic datatype **) |
13 (** the basic datatype **) |
14 type state |
14 type state |
15 val e_state: state |
15 val e_state: state |
44 val is_pblnd : ctree -> bool |
44 val is_pblnd : ctree -> bool |
45 |
45 |
46 val g_spec : ppobj -> References_Def.T |
46 val g_spec : ppobj -> References_Def.T |
47 val g_loc : ppobj -> (Istate_Def.T * Proof.context) option * (Istate_Def.T * Proof.context) option |
47 val g_loc : ppobj -> (Istate_Def.T * Proof.context) option * (Istate_Def.T * Proof.context) option |
48 val g_form : ppobj -> term |
48 val g_form : ppobj -> term |
49 val g_pbl : ppobj -> Model_Def.i_model_TEST |
49 val g_pbl : ppobj -> Model_Def.i_model_POS |
50 val g_met : ppobj -> Model_Def.i_model_TEST |
50 val g_met : ppobj -> Model_Def.i_model_POS |
51 val g_metID : ppobj -> MethodC.id |
51 val g_metID : ppobj -> MethodC.id |
52 val g_result : ppobj -> Celem.result |
52 val g_result : ppobj -> Celem.result |
53 val g_tac : ppobj -> Tactic.input |
53 val g_tac : ppobj -> Tactic.input |
54 val g_domID : ppobj -> ThyC.id |
54 val g_domID : ppobj -> ThyC.id |
55 |
55 |
179 {fmz : Model_Def.form_T, (* for uniformity also created/used for/by Subproblem *) |
179 {fmz : Model_Def.form_T, (* for uniformity also created/used for/by Subproblem *) |
180 origin: (Model_Def.o_model) *(* = O_Model.T for efficiently checking input to I_Model *) |
180 origin: (Model_Def.o_model) *(* = O_Model.T for efficiently checking input to I_Model *) |
181 References_Def.T * (* updated by Refine_Tacitly *) |
181 References_Def.T * (* updated by Refine_Tacitly *) |
182 term, (* headline of calc-head, as calculated initially(!) *) |
182 term, (* headline of calc-head, as calculated initially(!) *) |
183 spec : References_Def.T, (* explicitly input *) |
183 spec : References_Def.T, (* explicitly input *) |
184 probl : Model_Def.i_model_TEST,(* = I_Model.T for interactive input to a Problem *) |
184 probl : Model_Def.i_model_POS,(* = I_Model.T for interactive input to a Problem *) |
185 meth : Model_Def.i_model_TEST,(* = I_Model.T for interactive input to a MethodC *) |
185 meth : Model_Def.i_model_POS,(* = I_Model.T for interactive input to a MethodC *) |
186 ctxt : Proof.context, (* used while specifying this (Sub-)Problem and MethodC *) |
186 ctxt : Proof.context, (* used while specifying this (Sub-)Problem and MethodC *) |
187 loc : (Istate_Def.T * Proof.context) option (* like in PrfObj, calling this SubProblem *) |
187 loc : (Istate_Def.T * Proof.context) option (* like in PrfObj, calling this SubProblem *) |
188 * (Istate_Def.T * Proof.context) option, (* like in PrfObj, finishing the SubProblem *) |
188 * (Istate_Def.T * Proof.context) option, (* like in PrfObj, finishing the SubProblem *) |
189 branch: branch, (* like PrfObj *) |
189 branch: branch, (* like PrfObj *) |
190 result: Celem.result, (* like PrfObj *) |
190 result: Celem.result, (* like PrfObj *) |