src/HOL/Ord.ML
changeset 6115 c70bce7deb0f
parent 6109 82b50115564c
child 6128 2acc5d36610c
     1.1 --- a/src/HOL/Ord.ML	Wed Jan 13 12:08:51 1999 +0100
     1.2 +++ b/src/HOL/Ord.ML	Wed Jan 13 12:16:34 1999 +0100
     1.3 @@ -27,7 +27,7 @@
     1.4  
     1.5  (** Reflexivity **)
     1.6  
     1.7 -Addsimps [order_refl];
     1.8 +AddIffs [order_refl];
     1.9  
    1.10  (*This form is useful with the classical reasoner*)
    1.11  Goal "!!x::'a::order. x = y ==> x <= y";