# HG changeset patch
# User paulson
# Date 905440642 -7200
# Node ID d853d1ac85a35503c1e57219a5045c382985eed3
# Parent  40a09282ba14252269c1d6464708824d4e0120f4
Adds order_refl, order_less_irrefl as simps, not as Iffs, to avoid PROOF FAILED

diff -r 40a09282ba14 -r d853d1ac85a3 src/HOL/Ord.ML
--- a/src/HOL/Ord.ML	Thu Sep 10 17:15:48 1998 +0200
+++ b/src/HOL/Ord.ML	Thu Sep 10 17:17:22 1998 +0200
@@ -6,6 +6,11 @@
 The type class for ordered types
 *)
 
+(*Tell Blast_tac about overloading of < and <= to reduce the risk of
+  its applying a rule for the wrong type*)
+Blast.overloaded ("op <", domain_type); 
+Blast.overloaded ("op <=", domain_type);
+
 (** mono **)
 
 val [prem] = Goalw [mono_def]
@@ -20,7 +25,7 @@
 
 section "Orders";
 
-AddIffs [order_refl];
+Addsimps [order_refl];
 
 (*This form is useful with the classical reasoner*)
 Goal "!!x::'a::order. x = y ==> x <= y";
@@ -31,11 +36,12 @@
 Goal "~ x < (x::'a::order)";
 by (simp_tac (simpset() addsimps [order_less_le]) 1);
 qed "order_less_irrefl";
-AddIffs [order_less_irrefl];
+Addsimps [order_less_irrefl];
 
 Goal "(x::'a::order) <= y = (x < y | x = y)";
 by (simp_tac (simpset() addsimps [order_less_le]) 1);
-by (Blast_tac 1);
+   (*NOT suitable for AddIffs, since it can cause PROOF FAILED*)
+by (blast_tac (claset() addSIs [order_refl]) 1);
 qed "order_le_less";
 
 (** min **)