Adding lessI to default claset
authorpaulson
Thu Nov 07 10:11:06 1996 +0100 (1996-11-07)
changeset 2164c87368fc736b
parent 2163 4d43e7486164
child 2165 63dfe7f19cad
Adding lessI to default claset
src/HOL/Nat.ML
     1.1 --- a/src/HOL/Nat.ML	Wed Nov 06 12:49:31 1996 +0100
     1.2 +++ b/src/HOL/Nat.ML	Thu Nov 07 10:11:06 1996 +0100
     1.3 @@ -215,7 +215,7 @@
     1.4  goalw Nat.thy [less_def] "n < Suc(n)";
     1.5  by (rtac (pred_natI RS r_into_trancl) 1);
     1.6  qed "lessI";
     1.7 -Addsimps [lessI];
     1.8 +AddIffs [lessI];
     1.9  
    1.10  (* i<j ==> i<Suc(j) *)
    1.11  val less_SucI = lessI RSN (2, less_trans);