equal
deleted
inserted
replaced
204 |
204 |
205 lemma cont_Iwhen3: "cont (\<lambda>s. Iwhen f g s)" |
205 lemma cont_Iwhen3: "cont (\<lambda>s. Iwhen f g s)" |
206 apply (rule contI) |
206 apply (rule contI) |
207 apply (drule ssum_chain_lemma, safe) |
207 apply (drule ssum_chain_lemma, safe) |
208 apply (simp add: contlub_cfun_arg [symmetric]) |
208 apply (simp add: contlub_cfun_arg [symmetric]) |
209 apply (simp add: Iwhen4) |
209 apply (simp add: Iwhen4 cont_cfun_arg) |
210 apply (simp add: contlub_cfun_arg) |
|
211 apply (simp add: thelubE chain_monofun) |
|
212 apply (simp add: contlub_cfun_arg [symmetric]) |
210 apply (simp add: contlub_cfun_arg [symmetric]) |
213 apply (simp add: Iwhen5) |
211 apply (simp add: Iwhen5 cont_cfun_arg) |
214 apply (simp add: contlub_cfun_arg) |
|
215 apply (simp add: thelubE chain_monofun) |
|
216 done |
212 done |
217 |
213 |
218 subsection {* Continuous versions of constants *} |
214 subsection {* Continuous versions of constants *} |
219 |
215 |
220 constdefs |
216 constdefs |