equal
deleted
inserted
replaced
14 |
14 |
15 definition "pd_basis = {S::'a compact_basis set. finite S \<and> S \<noteq> {}}" |
15 definition "pd_basis = {S::'a compact_basis set. finite S \<and> S \<noteq> {}}" |
16 |
16 |
17 typedef 'a pd_basis = "pd_basis :: 'a compact_basis set set" |
17 typedef 'a pd_basis = "pd_basis :: 'a compact_basis set set" |
18 unfolding pd_basis_def |
18 unfolding pd_basis_def |
19 apply (rule_tac x="{a}" for a in exI) |
19 apply (rule_tac x="{_}" in exI) |
20 apply simp |
20 apply simp |
21 done |
21 done |
22 |
22 |
23 lemma finite_Rep_pd_basis [simp]: "finite (Rep_pd_basis u)" |
23 lemma finite_Rep_pd_basis [simp]: "finite (Rep_pd_basis u)" |
24 by (insert Rep_pd_basis [of u, unfolded pd_basis_def]) simp |
24 by (insert Rep_pd_basis [of u, unfolded pd_basis_def]) simp |