src/HOL/Nat.ML
changeset 2099 c5f004bfcbab
parent 2081 c2da3ca231ab
child 2115 9709f9188549
     1.1 --- a/src/HOL/Nat.ML	Tue Oct 15 16:40:04 1996 +0200
     1.2 +++ b/src/HOL/Nat.ML	Wed Oct 16 10:37:17 1996 +0200
     1.3 @@ -425,6 +425,10 @@
     1.4    "m=n ==> nat_rec a f m = nat_rec a f n"
     1.5    (fn [prem] => [rtac (prem RS arg_cong) 1]);
     1.6  
     1.7 +qed_goal "expand_nat_case" Nat.thy
     1.8 +  "P(nat_case z s n) = ((n=0 --> P z) & (!m. n = Suc m --> P(s m)))"
     1.9 +  (fn _ => [nat_ind_tac "n" 1, ALLGOALS Asm_simp_tac]);
    1.10 +
    1.11  val prems = goalw Nat.thy [le_def] "~n<m ==> m<=(n::nat)";
    1.12  by (resolve_tac prems 1);
    1.13  qed "leI";