equal
deleted
inserted
replaced
250 end; |
250 end; |
251 |
251 |
252 (*Duplication of hazardous rules, for complete provers*) |
252 (*Duplication of hazardous rules, for complete provers*) |
253 fun dup_intr th = zero_var_indexes (th RS classical); |
253 fun dup_intr th = zero_var_indexes (th RS classical); |
254 |
254 |
255 fun dup_elim th = |
255 fun dup_elim th = |
256 th RSN (2, revcut_rl) |> assumption 2 |> Seq.hd |> |
256 (case try |
257 rule_by_tactic (TRYALL (etac revcut_rl)) |
257 (rule_by_tactic (TRYALL (etac revcut_rl))) |
258 handle _ => error ("Bad format for elimination rule\n" ^ string_of_thm th); |
258 (th RSN (2, revcut_rl) |> assumption 2 |> Seq.hd) of |
|
259 Some th' => th' |
|
260 | _ => error ("Bad format for elimination rule\n" ^ string_of_thm th)); |
259 |
261 |
260 |
262 |
261 (**** Classical rule sets ****) |
263 (**** Classical rule sets ****) |
262 |
264 |
263 datatype claset = |
265 datatype claset = |