equal
deleted
inserted
replaced
906 "size (b\<Colon>bool) = 0" by (cases b) auto |
906 "size (b\<Colon>bool) = 0" by (cases b) auto |
907 |
907 |
908 lemma nat_size [simp, code]: "size (n\<Colon>nat) = n" |
908 lemma nat_size [simp, code]: "size (n\<Colon>nat) = n" |
909 by (induct n) simp_all |
909 by (induct n) simp_all |
910 |
910 |
911 declare "prod.size" [noatp] |
911 declare "prod.size" [no_atp] |
912 |
912 |
913 lemma [code]: |
913 lemma [code]: |
914 "size (P :: 'a Predicate.pred) = 0" by (cases P) simp |
914 "size (P :: 'a Predicate.pred) = 0" by (cases P) simp |
915 |
915 |
916 lemma [code]: |
916 lemma [code]: |