| changeset 2164 | c87368fc736b |
| parent 2115 | 9709f9188549 |
| child 2268 | 79a2f085a7fd |
--- 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);