author | berghofe |
Tue, 18 Dec 2007 12:26:24 +0100 | |
changeset 25690 | 5226396bf261 |
parent 25689 | 4853eeb03158 |
child 25691 | 8f8d83af100a |
src/HOL/Nat.thy | file | annotate | diff | comparison | revisions |
--- a/src/HOL/Nat.thy Tue Dec 18 12:26:00 2007 +0100 +++ b/src/HOL/Nat.thy Tue Dec 18 12:26:24 2007 +0100 @@ -1152,7 +1152,7 @@ lemma size_bool [code func]: "size (b\<Colon>bool) = 0" by (cases b) auto -declare "*.size" [noatp] +declare "prod.size" [noatp] subsection {* Embedding of the Naturals into any