equal
deleted
inserted
replaced
4 *) |
4 *) |
5 |
5 |
6 header {* Countable sets *} |
6 header {* Countable sets *} |
7 |
7 |
8 theory Countable_Set |
8 theory Countable_Set |
9 imports "~~/src/HOL/Library/Countable" "~~/src/HOL/Library/Infinite_Set" |
9 imports Countable Infinite_Set |
10 begin |
10 begin |
11 |
11 |
12 subsection {* Predicate for countable sets *} |
12 subsection {* Predicate for countable sets *} |
13 |
13 |
14 definition countable :: "'a set \<Rightarrow> bool" where |
14 definition countable :: "'a set \<Rightarrow> bool" where |