equal
deleted
inserted
replaced
1 subsection \<open>Code setup for sets with cardinality type information\<close> |
1 section \<open>Code setup for sets with cardinality type information\<close> |
2 |
2 |
3 theory Code_Cardinality imports Cardinality begin |
3 theory Code_Cardinality imports Cardinality begin |
4 |
4 |
5 text \<open> |
5 text \<open> |
6 Implement \<^term>\<open>CARD('a)\<close> via \<^term>\<open>card_UNIV\<close> and provide |
6 Implement \<^term>\<open>CARD('a)\<close> via \<^term>\<open>card_UNIV\<close> and provide |