equal
deleted
inserted
replaced
202 in |
202 in |
203 |
203 |
204 fun classical_rule rule = |
204 fun classical_rule rule = |
205 if is_elim rule then |
205 if is_elim rule then |
206 let |
206 let |
|
207 val ntags = Thm.get_name_tags rule; |
207 val rule' = rule RS classical; |
208 val rule' = rule RS classical; |
208 val concl' = Thm.concl_of rule'; |
209 val concl' = Thm.concl_of rule'; |
209 fun redundant_hyp goal = |
210 fun redundant_hyp goal = |
210 equal_concl concl' goal orelse |
211 equal_concl concl' goal orelse |
211 (case Logic.strip_assums_hyp goal of |
212 (case Logic.strip_assums_hyp goal of |
215 rule' |> ALLGOALS (SUBGOAL (fn (goal, i) => |
216 rule' |> ALLGOALS (SUBGOAL (fn (goal, i) => |
216 if i = 1 orelse redundant_hyp goal |
217 if i = 1 orelse redundant_hyp goal |
217 then Tactic.etac thin_rl i |
218 then Tactic.etac thin_rl i |
218 else all_tac)) |
219 else all_tac)) |
219 |> Seq.hd |
220 |> Seq.hd |
220 |> Drule.zero_var_indexes; |
221 |> Drule.zero_var_indexes |
|
222 |> Thm.put_name_tags ntags; |
221 in if Drule.weak_eq_thm (rule, rule'') then rule else rule'' end |
223 in if Drule.weak_eq_thm (rule, rule'') then rule else rule'' end |
222 else rule; |
224 else rule; |
223 |
225 |
224 end; |
226 end; |
225 |
227 |