equal
deleted
inserted
replaced
118 lemmas dictionary_second_step = internalized_sort[unoverload "open :: 'a set \<Rightarrow> bool"] |
118 lemmas dictionary_second_step = internalized_sort[unoverload "open :: 'a set \<Rightarrow> bool"] |
119 text\<open>The theorem with internalized type classes and compiled out operations is the starting point |
119 text\<open>The theorem with internalized type classes and compiled out operations is the starting point |
120 for the original relativization algorithm.\<close> |
120 for the original relativization algorithm.\<close> |
121 thm dictionary_second_step |
121 thm dictionary_second_step |
122 |
122 |
|
123 text \<open>Alternative construction using \<open>unoverload_type\<close> |
|
124 (This does not require fiddling with \<open>Sign.add_const_constraint\<close>).\<close> |
|
125 lemmas dictionary_second_step' = dictionary_first_step[unoverload_type 'a] |
123 |
126 |
124 text\<open>This is the set-based variant of the theorem compact_imp_closed.\<close> |
127 text\<open>This is the set-based variant of the theorem compact_imp_closed.\<close> |
125 lemma compact_imp_closed_set_based: |
128 lemma compact_imp_closed_set_based: |
126 assumes "(A::'a set) \<noteq> {}" |
129 assumes "(A::'a set) \<noteq> {}" |
127 shows "\<forall>open. t2_space_on_with A open \<longrightarrow> (\<forall>S\<subseteq>A. compact_on_with A open S \<longrightarrow> |
130 shows "\<forall>open. t2_space_on_with A open \<longrightarrow> (\<forall>S\<subseteq>A. compact_on_with A open S \<longrightarrow> |