8 |
8 |
9 signature CONTEXT_RULES = |
9 signature CONTEXT_RULES = |
10 sig |
10 sig |
11 type netpair |
11 type netpair |
12 type T |
12 type T |
13 val netpair_bang: ProofContext.context -> netpair |
13 val netpair_bang: Proof.context -> netpair |
14 val netpair: ProofContext.context -> netpair |
14 val netpair: Proof.context -> netpair |
15 val orderlist: ((int * int) * 'a) list -> 'a list |
15 val orderlist: ((int * int) * 'a) list -> 'a list |
16 val find_rules_netpair: bool -> thm list -> term -> netpair -> thm list |
16 val find_rules_netpair: bool -> thm list -> term -> netpair -> thm list |
17 val find_rules: bool -> thm list -> term -> ProofContext.context -> thm list list |
17 val find_rules: bool -> thm list -> term -> Proof.context -> thm list list |
18 val print_rules: Context.generic -> unit |
18 val print_rules: Context.generic -> unit |
19 val addSWrapper: ((int -> tactic) -> int -> tactic) -> theory -> theory |
19 val addSWrapper: ((int -> tactic) -> int -> tactic) -> theory -> theory |
20 val addWrapper: ((int -> tactic) -> int -> tactic) -> theory -> theory |
20 val addWrapper: ((int -> tactic) -> int -> tactic) -> theory -> theory |
21 val Swrap: ProofContext.context -> (int -> tactic) -> int -> tactic |
21 val Swrap: Proof.context -> (int -> tactic) -> int -> tactic |
22 val wrap: ProofContext.context -> (int -> tactic) -> int -> tactic |
22 val wrap: Proof.context -> (int -> tactic) -> int -> tactic |
23 val intro_bang: int option -> attribute |
23 val intro_bang: int option -> attribute |
24 val elim_bang: int option -> attribute |
24 val elim_bang: int option -> attribute |
25 val dest_bang: int option -> attribute |
25 val dest_bang: int option -> attribute |
26 val intro: int option -> attribute |
26 val intro: int option -> attribute |
27 val elim: int option -> attribute |
27 val elim: int option -> attribute |