Addition of le_refl to default simpset/claset
authorpaulson
Mon Sep 23 18:12:45 1996 +0200 (1996-09-23)
changeset 20099023e474d22a
parent 2008 cd81b719142d
child 2010 0a22b9d63a18
Addition of le_refl to default simpset/claset
src/HOL/Nat.ML
     1.1 --- a/src/HOL/Nat.ML	Mon Sep 23 18:10:48 1996 +0200
     1.2 +++ b/src/HOL/Nat.ML	Mon Sep 23 18:12:45 1996 +0200
     1.3 @@ -517,7 +517,7 @@
     1.4  by (simp_tac (!simpset addsimps [le_eq_less_or_eq]) 1);
     1.5  qed "Suc_le_mono";
     1.6  
     1.7 -Addsimps [le_refl,Suc_le_mono];
     1.8 +AddIffs [le_refl,Suc_le_mono];
     1.9  
    1.10  
    1.11  (** LEAST -- the least number operator **)