equal
deleted
inserted
replaced
129 (Proof.context -> int -> tactic) -> (Proof.context -> Proof.method) context_parser |
129 (Proof.context -> int -> tactic) -> (Proof.context -> Proof.method) context_parser |
130 val setup: theory -> theory |
130 val setup: theory -> theory |
131 end; |
131 end; |
132 |
132 |
133 |
133 |
134 functor ClassicalFun(Data: CLASSICAL_DATA): CLASSICAL = |
134 functor Classical(Data: CLASSICAL_DATA): CLASSICAL = |
135 struct |
135 struct |
136 |
136 |
137 (** classical elimination rules **) |
137 (** classical elimination rules **) |
138 |
138 |
139 (* |
139 (* |