| changeset 56375 | 32e0da92c786 |
| parent 56218 | 1c3f1f2431f9 |
| child 56643 | 41d3596d8a64 |
| 56374:dfc7a46c2900 | 56375:32e0da92c786 |
|---|---|
857 "size (b\<Colon>bool) = 0" by (cases b) auto |
857 "size (b\<Colon>bool) = 0" by (cases b) auto |
858 |
858 |
859 lemma nat_size [simp, code]: "size (n\<Colon>nat) = n" |
859 lemma nat_size [simp, code]: "size (n\<Colon>nat) = n" |
860 by (induct n) simp_all |
860 by (induct n) simp_all |
861 |
861 |
862 declare "prod.size" [no_atp] |
862 declare prod.size [no_atp] |
863 |
863 |
864 |
864 |
865 hide_const (open) acc accp |
865 hide_const (open) acc accp |
866 |
866 |
867 end |
867 end |