# HG changeset patch # User paulson # Date 864732233 -7200 # Node ID 0d955bcf8e0a4ef619f2bb40c6d65772fa141375 # Parent 3dac856935474b1f67b9c49fc21b8464c14f5ccf New theorem le_Suc_eq diff -r 3dac85693547 -r 0d955bcf8e0a src/HOL/NatDef.ML --- a/src/HOL/NatDef.ML Tue May 27 13:23:27 1997 +0200 +++ b/src/HOL/NatDef.ML Tue May 27 13:23:53 1997 +0200 @@ -423,6 +423,11 @@ n_not_Suc_n, Suc_n_not_n, nat_case_0, nat_case_Suc, nat_rec_0, nat_rec_Suc]; +goal thy "!!m. (m <= Suc(n)) = (m<=n | m = Suc n)"; +by (simp_tac (!simpset addsimps [le_eq_less_Suc]) 1); +by (blast_tac (!claset addSEs [less_SucE] addIs [less_SucI]) 1); +qed "le_Suc_eq"; + (* goal thy "(Suc m < n | Suc m = n) = (m < n)"; by (stac (less_Suc_eq RS sym) 1);