src/HOL/Nat.ML
changeset 11337 9d6d6a8966b9
parent 11139 b092ad5cd510
child 11464 ddea204de5bc
     1.1 --- a/src/HOL/Nat.ML	Thu May 31 16:50:04 2001 +0200
     1.2 +++ b/src/HOL/Nat.ML	Thu May 31 16:50:13 2001 +0200
     1.3 @@ -94,6 +94,11 @@
     1.4  by (blast_tac (claset() addIs [order_antisym]) 1); 
     1.5  qed "Least_Suc";
     1.6  
     1.7 +Goal "[|P n; Q m; ~P 0; !k. P (Suc k) = Q k|] ==> Least P = Suc (Least Q)";
     1.8 +by (eatac (Least_Suc RS ssubst) 1 1);
     1.9 +by (Asm_simp_tac 1);
    1.10 +qed "Least_Suc2";
    1.11 +
    1.12  
    1.13  (** min and max **)
    1.14