equal
deleted
inserted
replaced
2825 | first_is_neg lhs rhs (thm::thms) = |
2825 | first_is_neg lhs rhs (thm::thms) = |
2826 (case Thm.prop_of thm of |
2826 (case Thm.prop_of thm of |
2827 _ $ (@{term "HOL.Not"} $ (Const ("HOL.eq", _) $ l $ r)) => |
2827 _ $ (@{term "HOL.Not"} $ (Const ("HOL.eq", _) $ l $ r)) => |
2828 (if l = lhs andalso r = rhs then SOME(thm) |
2828 (if l = lhs andalso r = rhs then SOME(thm) |
2829 else if r = lhs andalso l = rhs then SOME(thm RS @{thm not_sym}) |
2829 else if r = lhs andalso l = rhs then SOME(thm RS @{thm not_sym}) |
2830 else NONE) |
2830 else first_is_neg lhs rhs thms) |
2831 | _ => first_is_neg lhs rhs thms) |
2831 | _ => first_is_neg lhs rhs thms) |
2832 |
2832 |
2833 val simp_thms = @{thms fresh_Pair fresh_at_base atom_eq_iff} |
2833 val simp_thms = @{thms fresh_Pair fresh_at_base atom_eq_iff} |
2834 val prems = Simplifier.prems_of ss |
2834 val prems = Simplifier.prems_of ss |
2835 |> filter (fn thm => case Thm.prop_of thm of |
2835 |> filter (fn thm => case Thm.prop_of thm of |