# HG changeset patch
# User paulson
# Date 847357866 -3600
# Node ID c87368fc736bf00e2446fe45b5a0a7ffa7b1e875
# Parent  4d43e7486164b7a38bba4c0d8de9348c24cfd3d0
Adding lessI to default claset

diff -r 4d43e7486164 -r c87368fc736b src/HOL/Nat.ML
--- a/src/HOL/Nat.ML	Wed Nov 06 12:49:31 1996 +0100
+++ b/src/HOL/Nat.ML	Thu Nov 07 10:11:06 1996 +0100
@@ -215,7 +215,7 @@
 goalw Nat.thy [less_def] "n < Suc(n)";
 by (rtac (pred_natI RS r_into_trancl) 1);
 qed "lessI";
-Addsimps [lessI];
+AddIffs [lessI];
 
 (* i<j ==> i<Suc(j) *)
 val less_SucI = lessI RSN (2, less_trans);