# HG changeset patch
# User paulson
# Date 840448171 -7200
# Node ID d94c12235878743a125dba6b80e68b7ef8f4d93b
# Parent  d898eb4beb967ce9f530b981fac866e52145d473
Now less_zeroE is a Safe Elim rule

diff -r d898eb4beb96 -r d94c12235878 src/HOL/Nat.ML
--- 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";