equal
deleted
inserted
replaced
14 val check: Tactic.input -> Calc.T -> Applicable.T |
14 val check: Tactic.input -> Calc.T -> Applicable.T |
15 val add: Tactic.T -> Istate_Def.T * Proof.context -> Calc.T -> Test_Out.T |
15 val add: Tactic.T -> Istate_Def.T * Proof.context -> Calc.T -> Test_Out.T |
16 |
16 |
17 val inconsistent: Subst.input option * ThmC.T -> term -> Istate_Def.T * Proof.context -> |
17 val inconsistent: Subst.input option * ThmC.T -> term -> Istate_Def.T * Proof.context -> |
18 Pos.pos' -> Ctree.ctree -> Calc.T |
18 Pos.pos' -> Ctree.ctree -> Calc.T |
|
19 |
19 \<^isac_test>\<open> |
20 \<^isac_test>\<open> |
20 val specify_do_next: Calc.T -> string * Calc.state_post |
21 val specify_do_next: Calc.T -> string * Calc.state_post |
21 val switch_specify_solve: Pos.pos_ -> Calc.T -> string * Calc.state_post |
22 val switch_specify_solve: Pos.pos_ -> Calc.T -> string * Calc.state_post |
22 \<close> |
23 \<close> |
23 end |
24 end |