src/HOL/Nat.ML
changeset 1475 7f5a4cd08209
parent 1465 5d7a7e439cec
child 1485 240cc98b94a7
     1.1 --- a/src/HOL/Nat.ML	Mon Feb 05 14:44:09 1996 +0100
     1.2 +++ b/src/HOL/Nat.ML	Mon Feb 05 21:27:16 1996 +0100
     1.3 @@ -160,7 +160,17 @@
     1.4  
     1.5  (*** nat_rec -- by wf recursion on pred_nat ***)
     1.6  
     1.7 -bind_thm ("nat_rec_unfold", (wf_pred_nat RS (nat_rec_def RS def_wfrec)));
     1.8 +(* The unrolling rule for nat_rec *)
     1.9 +goal Nat.thy
    1.10 +   "(%n. nat_rec n c d) = wfrec pred_nat (%f. nat_case ?c (%m. ?d m (f m)))";
    1.11 +  by (simp_tac (HOL_ss addsimps [nat_rec_def]) 1);
    1.12 +bind_thm("nat_rec_unfold", wf_pred_nat RS 
    1.13 +                            ((result() RS eq_reflection) RS def_wfrec));
    1.14 +
    1.15 +(*---------------------------------------------------------------------------
    1.16 + * Old:
    1.17 + * bind_thm ("nat_rec_unfold", (wf_pred_nat RS (nat_rec_def RS def_wfrec))); 
    1.18 + *---------------------------------------------------------------------------*)
    1.19  
    1.20  (** conversion rules **)
    1.21