author | haftmann |
Mon, 30 Jun 2008 13:41:28 +0200 | |
changeset 27395 | 67330748a72e |
parent 27394 | facb528f1834 |
child 27396 | 77ea650bfc3a |
src/HOL/Int.thy | file | annotate | diff | comparison | revisions |
--- a/src/HOL/Int.thy Sat Jun 28 23:52:43 2008 +0200 +++ b/src/HOL/Int.thy Mon Jun 30 13:41:28 2008 +0200 @@ -1924,7 +1924,7 @@ lemmas int_aux_code = of_nat_aux_code [where ?'a = int, simplified int_aux_def [symmetric], code] lemma [code, code unfold, code inline del]: - "of_nat n = int_aux n 0" + "of_nat = (\<lambda>n. int_aux n 0)" by (simp add: int_aux_def of_nat_aux_def) definition