equal
deleted
inserted
replaced
53 val erule: Proof.context -> int -> thm list -> method |
53 val erule: Proof.context -> int -> thm list -> method |
54 val drule: Proof.context -> int -> thm list -> method |
54 val drule: Proof.context -> int -> thm list -> method |
55 val frule: Proof.context -> int -> thm list -> method |
55 val frule: Proof.context -> int -> thm list -> method |
56 val set_tactic: (morphism -> thm list -> tactic) -> Context.generic -> Context.generic |
56 val set_tactic: (morphism -> thm list -> tactic) -> Context.generic -> Context.generic |
57 val clean_facts: thm list -> thm list |
57 val clean_facts: thm list -> thm list |
58 val get_facts: Proof.context -> thm list |
|
59 val update_facts: (thm list -> thm list) -> Proof.context -> Proof.context |
|
60 type combinator_info |
58 type combinator_info |
61 val no_combinator_info: combinator_info |
59 val no_combinator_info: combinator_info |
62 datatype combinator = Then | Then_All_New | Orelse | Try | Repeat1 | Select_Goals of int |
60 datatype combinator = Then | Then_All_New | Orelse | Try | Repeat1 | Select_Goals of int |
63 datatype text = |
61 datatype text = |
64 Source of Token.src | |
62 Source of Token.src | |