equal
deleted
inserted
replaced
222 |
222 |
223 fun dup_elim th = |
223 fun dup_elim th = |
224 (case try (fn () => |
224 (case try (fn () => |
225 rule_by_tactic (TRYALL (etac revcut_rl)) |
225 rule_by_tactic (TRYALL (etac revcut_rl)) |
226 (th RSN (2, revcut_rl) |> assumption 2 |> Seq.hd)) () of |
226 (th RSN (2, revcut_rl) |> assumption 2 |> Seq.hd)) () of |
227 Some th' => th' |
227 SOME th' => th' |
228 | _ => error ("Bad format for elimination rule\n" ^ string_of_thm th)); |
228 | _ => error ("Bad format for elimination rule\n" ^ string_of_thm th)); |
229 |
229 |
230 |
230 |
231 (**** Classical rule sets ****) |
231 (**** Classical rule sets ****) |
232 |
232 |