# HG changeset patch
# User paulson
# Date 886672049 -3600
# Node ID e3e7e901ce6c34220658098c3af1b1f69be5acc1
# Parent  3a4348a3d6ffccb43d7af80ef6ce367df96ce2a0
New theorem order_eq_refl

diff -r 3a4348a3d6ff -r e3e7e901ce6c src/HOL/Ord.ML
--- 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";