equal
deleted
inserted
replaced
29 val thms_of_rls : rls -> rule list |
29 val thms_of_rls : rls -> rule list |
30 val theID2filename : theID -> filename |
30 val theID2filename : theID -> filename |
31 val no_thycontext : guh -> bool |
31 val no_thycontext : guh -> bool |
32 val subs_from : Ctree.istate -> 'a -> guh -> Ctree.subs |
32 val subs_from : Ctree.istate -> 'a -> guh -> Ctree.subs |
33 val guh2rewtac : guh -> Ctree.subs -> Ctree.tac |
33 val guh2rewtac : guh -> Ctree.subs -> Ctree.tac |
34 val get_tac_checked : Ctree.ptree -> Ctree.pos' -> Ctree.tac |
34 val get_tac_checked : Ctree.ctree -> Ctree.pos' -> Ctree.tac |
35 val context_thy : Ctree.ptree * Ctree.pos' -> Ctree.tac -> contthy |
35 val context_thy : Ctree.ctree * Ctree.pos' -> Ctree.tac -> contthy |
36 val distinct_Thm : rule list -> rule list |
36 val distinct_Thm : rule list -> rule list |
37 val eq_Thms : string list -> rule -> bool |
37 val eq_Thms : string list -> rule -> bool |
38 val make_deriv : theory -> rls -> rule list -> ((term * term) list -> term * term -> bool) -> |
38 val make_deriv : theory -> rls -> rule list -> ((term * term) list -> term * term -> bool) -> |
39 term option -> term -> deriv |
39 term option -> term -> deriv |
40 val reverse_deriv : theory -> rls -> rule list -> ((term * term) list -> term * term -> bool) -> |
40 val reverse_deriv : theory -> rls -> rule list -> ((term * term) list -> term * term -> bool) -> |