# HG changeset patch
# User oheimb
# Date 991320613 -7200
# Node ID 9d6d6a8966b91bdf8a8e178943f47864336224f4
# Parent  fedccaeb52675d85e44535a557d7bbc0acbe26c4
added Least_Suc2

diff -r fedccaeb5267 -r 9d6d6a8966b9 src/HOL/Nat.ML
--- a/src/HOL/Nat.ML	Thu May 31 16:50:04 2001 +0200
+++ b/src/HOL/Nat.ML	Thu May 31 16:50:13 2001 +0200
@@ -94,6 +94,11 @@
 by (blast_tac (claset() addIs [order_antisym]) 1); 
 qed "Least_Suc";
 
+Goal "[|P n; Q m; ~P 0; !k. P (Suc k) = Q k|] ==> Least P = Suc (Least Q)";
+by (eatac (Least_Suc RS ssubst) 1 1);
+by (Asm_simp_tac 1);
+qed "Least_Suc2";
+
 
 (** min and max **)