equal
deleted
inserted
replaced
649 -- {* This form is useful with the classical reasoner. *} |
649 -- {* This form is useful with the classical reasoner. *} |
650 apply (erule ssubst) |
650 apply (erule ssubst) |
651 apply (rule order_refl) |
651 apply (rule order_refl) |
652 done |
652 done |
653 |
653 |
654 lemma order_less_irrefl [simp]: "~ x < (x::'a::order)" |
654 lemma order_less_irrefl [iff]: "~ x < (x::'a::order)" |
655 by (simp add: order_less_le) |
655 by (simp add: order_less_le) |
656 |
656 |
657 lemma order_le_less: "((x::'a::order) <= y) = (x < y | x = y)" |
657 lemma order_le_less: "((x::'a::order) <= y) = (x < y | x = y)" |
658 -- {* NOT suitable for iff, since it can cause PROOF FAILED. *} |
658 -- {* NOT suitable for iff, since it can cause PROOF FAILED. *} |
659 apply (simp add: order_less_le) |
659 apply (simp add: order_less_le) |