equal
deleted
inserted
replaced
2733 | first_is_neg lhs rhs (thm::thms) = |
2733 | first_is_neg lhs rhs (thm::thms) = |
2734 (case Thm.prop_of thm of |
2734 (case Thm.prop_of thm of |
2735 _ $ (@{term "HOL.Not"} $ (Const ("HOL.eq", _) $ l $ r)) => |
2735 _ $ (@{term "HOL.Not"} $ (Const ("HOL.eq", _) $ l $ r)) => |
2736 (if l = lhs andalso r = rhs then SOME(thm) |
2736 (if l = lhs andalso r = rhs then SOME(thm) |
2737 else if r = lhs andalso l = rhs then SOME(thm RS @{thm not_sym}) |
2737 else if r = lhs andalso l = rhs then SOME(thm RS @{thm not_sym}) |
2738 else NONE) |
2738 else first_is_neg lhs rhs thms) |
2739 | _ => first_is_neg lhs rhs thms) |
2739 | _ => first_is_neg lhs rhs thms) |
2740 |
2740 |
2741 val simp_thms = @{thms fresh_Pair fresh_at_base atom_eq_iff} |
2741 val simp_thms = @{thms fresh_Pair fresh_at_base atom_eq_iff} |
2742 val prems = Simplifier.prems_of ss |
2742 val prems = Simplifier.prems_of ss |
2743 |> filter (fn thm => case Thm.prop_of thm of |
2743 |> filter (fn thm => case Thm.prop_of thm of |