src/HOL/Nat.thy
changeset 55642 63beb38e9258
parent 55575 a5e33e18fb5c
child 56020 f92479477c52
     1.1 --- a/src/HOL/Nat.thy	Fri Feb 21 00:09:55 2014 +0100
     1.2 +++ b/src/HOL/Nat.thy	Fri Feb 21 00:09:56 2014 +0100
     1.3 @@ -112,9 +112,8 @@
     1.4  
     1.5  lemmas induct = old.nat.induct
     1.6  lemmas inducts = old.nat.inducts
     1.7 -lemmas recs = old.nat.recs
     1.8 -lemmas cases = nat.case
     1.9 -lemmas simps = nat.inject nat.distinct nat.case old.nat.recs
    1.10 +lemmas rec = old.nat.rec
    1.11 +lemmas simps = nat.inject nat.distinct nat.case nat.rec
    1.12  
    1.13  setup {* Sign.parent_path *}
    1.14