equal
deleted
inserted
replaced
846 apply(drule assms) |
846 apply(drule assms) |
847 apply (blast intro: card_mono finite_subset psubset_card_mono dest: psubset_eq[THEN iffD2]) |
847 apply (blast intro: card_mono finite_subset psubset_card_mono dest: psubset_eq[THEN iffD2]) |
848 done |
848 done |
849 |
849 |
850 |
850 |
851 subsection {* size of a datatype value *} |
|
852 |
|
853 ML_file "Tools/Function/size.ML" |
|
854 setup Size.setup |
|
855 |
|
856 lemma size_bool [code]: |
|
857 "size (b\<Colon>bool) = 0" by (cases b) auto |
|
858 |
|
859 lemma nat_size [simp, code]: "size (n\<Colon>nat) = n" |
|
860 by (induct n) simp_all |
|
861 |
|
862 declare prod.size [no_atp] |
|
863 |
|
864 |
|
865 hide_const (open) acc accp |
851 hide_const (open) acc accp |
866 |
852 |
867 end |
853 end |