equal
deleted
inserted
replaced
110 old.nat.inject[iff del] |
110 old.nat.inject[iff del] |
111 old.nat.distinct(1)[simp del, induct_simp del] |
111 old.nat.distinct(1)[simp del, induct_simp del] |
112 |
112 |
113 lemmas induct = old.nat.induct |
113 lemmas induct = old.nat.induct |
114 lemmas inducts = old.nat.inducts |
114 lemmas inducts = old.nat.inducts |
115 lemmas recs = old.nat.recs |
115 lemmas rec = old.nat.rec |
116 lemmas cases = nat.case |
116 lemmas simps = nat.inject nat.distinct nat.case nat.rec |
117 lemmas simps = nat.inject nat.distinct nat.case old.nat.recs |
|
118 |
117 |
119 setup {* Sign.parent_path *} |
118 setup {* Sign.parent_path *} |
120 |
119 |
121 abbreviation rec_nat :: "'a \<Rightarrow> (nat \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a" where |
120 abbreviation rec_nat :: "'a \<Rightarrow> (nat \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a" where |
122 "rec_nat \<equiv> old.rec_nat" |
121 "rec_nat \<equiv> old.rec_nat" |