| changeset 4600 | e3e7e901ce6c |
| parent 4089 | 96fba19bcbe2 |
| child 4640 | ac6cf9f18653 |
--- a/src/HOL/Ord.ML Thu Feb 05 10:46:31 1998 +0100 +++ b/src/HOL/Ord.ML Thu Feb 05 10:47:29 1998 +0100 @@ -24,6 +24,12 @@ AddIffs [order_refl]; +(*This form is useful with the classical reasoner*) +goal Ord.thy "!!x::'a::order. x = y ==> x <= y"; +by (etac ssubst 1); +by (rtac order_refl 1); +qed "order_eq_refl"; + goal Ord.thy "~ x < (x::'a::order)"; by (simp_tac (simpset() addsimps [order_less_le]) 1); qed "order_less_irrefl";