--- a/src/HOL/Nat.ML Mon Aug 19 11:33:08 1996 +0200
+++ b/src/HOL/Nat.ML Mon Aug 19 11:49:31 1996 +0200
@@ -269,6 +269,7 @@
(* n<0 ==> R *)
bind_thm ("less_zeroE", (not_less0 RS notE));
+AddSEs [less_zeroE];
val [major,less,eq] = goal Nat.thy
"[| m < Suc(n); m<n ==> P; m=n ==> P |] ==> P";
@@ -281,7 +282,7 @@
goal Nat.thy "(m < Suc(n)) = (m < n | m = n)";
by (fast_tac (!claset addSIs [lessI]
- addEs [less_trans, less_SucE]) 1);
+ addEs [less_trans, less_SucE]) 1);
qed "less_Suc_eq";
val prems = goal Nat.thy "m<n ==> n ~= 0";