src/HOL/Datatype.thy
changeset 26072 f65a7fa2da6c
parent 25836 f7771e4f7064
child 26146 61cb176d0385
     1.1 --- a/src/HOL/Datatype.thy	Fri Feb 15 16:09:10 2008 +0100
     1.2 +++ b/src/HOL/Datatype.thy	Fri Feb 15 16:09:12 2008 +0100
     1.3 @@ -12,6 +12,11 @@
     1.4  imports Finite_Set
     1.5  begin
     1.6  
     1.7 +lemma size_bool [code func]:
     1.8 +  "size (b\<Colon>bool) = 0" by (cases b) auto
     1.9 +
    1.10 +declare "prod.size" [noatp]
    1.11 +
    1.12  typedef (Node)
    1.13    ('a,'b) node = "{p. EX f x k. p = (f::nat=>'b+nat, x::'a+nat) & f k = Inr 0}"
    1.14      --{*it is a subtype of @{text "(nat=>'b+nat) * ('a+nat)"}*}