equal
deleted
inserted
replaced
78 "sort_of (a:::name) = Sort ''name'' []" |
78 "sort_of (a:::name) = Sort ''name'' []" |
79 |
79 |
80 This does not work for multi-sorted atoms. |
80 This does not work for multi-sorted atoms. |
81 *} |
81 *} |
82 |
82 |
|
83 (* fixme |
|
84 lemma supp_of_finite_name_set: |
|
85 fixes S::"name set" |
|
86 assumes "infinte S" "infinite (UNIV - S)" |
|
87 shows "supp S = UNIV" |
|
88 proof - |
|
89 { fix a |
|
90 have "a \<in> supp S" |
|
91 proof (cases "a \<in> atom ` S") |
|
92 assume "a \<in> atom ` S" |
|
93 then have "\<forall>b \<in> UNIV - S. (a \<rightleftharpoons> atom b) \<bullet> S \<noteq> S" |
|
94 apply(clarify) |
|
95 |
|
96 show "a \<in> supp S" |
|
97 } |
|
98 then show "supp S = UNIV" by auto |
|
99 qed |
|
100 *) |
|
101 |
83 |
102 |
84 section {* Automatic instantiation of class @{text at}. *} |
103 section {* Automatic instantiation of class @{text at}. *} |
85 |
104 |
86 atom_decl name2 |
105 atom_decl name2 |
87 |
106 |