equal
deleted
inserted
replaced
16 val implicit_take : Program.T -> (term * term) list -> term option |
16 val implicit_take : Program.T -> (term * term) list -> term option |
17 val init_pstate : Rule_Set.T -> Proof.context -> Model.itm list -> Celem.metID -> |
17 val init_pstate : Rule_Set.T -> Proof.context -> Model.itm list -> Celem.metID -> |
18 Istate.T * Proof.context * Program.T |
18 Istate.T * Proof.context * Program.T |
19 |
19 |
20 val get_simplifier : Calc.T -> Rule_Set.T |
20 val get_simplifier : Calc.T -> Rule_Set.T |
21 val resume_prog : ThyC.theory' (*..for lookup in KEStore*) -> Pos.pos' -> Ctree.ctree -> |
21 val resume_prog : ThyC.id (*..for lookup in KEStore*) -> Pos.pos' -> Ctree.ctree -> |
22 (Istate.T * Proof.context) * Program.T |
22 (Istate.T * Proof.context) * Program.T |
23 |
23 |
24 val tac_from_prog : Ctree.ctree -> theory (*..for lookup in KEStore*) -> term -> Tactic.input |
24 val tac_from_prog : Ctree.ctree -> theory (*..for lookup in KEStore*) -> term -> Tactic.input |
25 val check_leaf : string -> Proof.context -> Rule_Set.T -> (Env.T * (term option * term)) -> term -> |
25 val check_leaf : string -> Proof.context -> Rule_Set.T -> (Env.T * (term option * term)) -> term -> |
26 Program.leaf * term option |
26 Program.leaf * term option |