equal
deleted
inserted
replaced
10 val item_to_add: Proof.context -> O_Model.T -> I_Model.T_POS -> |
10 val item_to_add: Proof.context -> O_Model.T -> I_Model.T_POS -> |
11 (Model_Def.m_field * TermC.as_string) option |
11 (Model_Def.m_field * TermC.as_string) option |
12 val by_Add_: string -> TermC.as_string -> Calc.T -> string * Calc.state_post |
12 val by_Add_: string -> TermC.as_string -> Calc.T -> string * Calc.state_post |
13 |
13 |
14 (*from isac_test for Minisubpbl*) |
14 (*from isac_test for Minisubpbl*) |
15 (*OLD*) |
|
16 val for_problem: Proof.context -> O_Model.T -> References.T * References.T -> I_Model.T_POS * I_Model.T_POS -> |
15 val for_problem: Proof.context -> O_Model.T -> References.T * References.T -> I_Model.T_POS * I_Model.T_POS -> |
17 string * (Pos.pos_ * Tactic.input) |
16 string * (Pos.pos_ * Tactic.input) |
18 val for_method: Proof.context -> O_Model.T -> References.T * References.T -> I_Model.T_POS * I_Model.T_POS -> |
17 val for_method: Proof.context -> O_Model.T -> References.T * References.T -> I_Model.T_POS * I_Model.T_POS -> |
19 string * (Pos.pos_ * Tactic.input) |
18 string * (Pos.pos_ * Tactic.input) |
20 (*---*) |
|
21 (*NEW*) |
|
22 val select_inc_lists: I_Model.T_POS -> I_Model.T_POS |
19 val select_inc_lists: I_Model.T_POS -> I_Model.T_POS |
23 |
20 |
24 \<^isac_test>\<open> |
21 \<^isac_test>\<open> |
25 (**) |
22 (**) |
26 \<close> |
23 \<close> |