equal
deleted
inserted
replaced
205 |
205 |
206 Goalw [stable_def] "F : stable A ==> F : A co A"; |
206 Goalw [stable_def] "F : stable A ==> F : A co A"; |
207 by (assume_tac 1); |
207 by (assume_tac 1); |
208 qed "stableD"; |
208 qed "stableD"; |
209 |
209 |
|
210 Goalw [stable_def, constrains_def] "stable UNIV = UNIV"; |
|
211 by Auto_tac; |
|
212 qed "stable_UNIV"; |
|
213 Addsimps [stable_UNIV]; |
|
214 |
210 (** Union **) |
215 (** Union **) |
211 |
216 |
212 Goalw [stable_def] |
217 Goalw [stable_def] |
213 "[| F : stable A; F : stable A' |] ==> F : stable (A Un A')"; |
218 "[| F : stable A; F : stable A' |] ==> F : stable (A Un A')"; |
214 by (blast_tac (claset() addIs [constrains_Un]) 1); |
219 by (blast_tac (claset() addIs [constrains_Un]) 1); |