equal
deleted
inserted
replaced
46 val set_mksym: (Proof.context -> thm -> thm option) -> Proof.context -> Proof.context |
46 val set_mksym: (Proof.context -> thm -> thm option) -> Proof.context -> Proof.context |
47 val set_mkeqTrue: (Proof.context -> thm -> thm option) -> Proof.context -> Proof.context |
47 val set_mkeqTrue: (Proof.context -> thm -> thm option) -> Proof.context -> Proof.context |
48 val set_termless: (term * term -> bool) -> Proof.context -> Proof.context |
48 val set_termless: (term * term -> bool) -> Proof.context -> Proof.context |
49 val set_subgoaler: (Proof.context -> int -> tactic) -> Proof.context -> Proof.context |
49 val set_subgoaler: (Proof.context -> int -> tactic) -> Proof.context -> Proof.context |
50 type trace_ops |
50 type trace_ops |
51 val set_trace_ops: trace_ops -> Proof.context -> Proof.context |
51 val set_trace_ops: trace_ops -> theory -> theory |
52 val simproc_global_i: theory -> string -> term list -> |
52 val simproc_global_i: theory -> string -> term list -> |
53 (Proof.context -> term -> thm option) -> simproc |
53 (Proof.context -> term -> thm option) -> simproc |
54 val simproc_global: theory -> string -> string list -> |
54 val simproc_global: theory -> string -> string list -> |
55 (Proof.context -> term -> thm option) -> simproc |
55 (Proof.context -> term -> thm option) -> simproc |
56 val rewrite: Proof.context -> conv |
56 val rewrite: Proof.context -> conv |