equal
deleted
inserted
replaced
190 by simp |
190 by simp |
191 |
191 |
192 subsection {* Continuity of application *} |
192 subsection {* Continuity of application *} |
193 |
193 |
194 lemma cont_Rep_cfun1: "cont (\<lambda>f. f\<cdot>x)" |
194 lemma cont_Rep_cfun1: "cont (\<lambda>f. f\<cdot>x)" |
195 by (rule cont_Rep_cfun [THEN cont2cont_fun]) |
195 by (rule cont_Rep_cfun [OF cont_id, THEN cont2cont_fun]) |
196 |
196 |
197 lemma cont_Rep_cfun2: "cont (\<lambda>x. f\<cdot>x)" |
197 lemma cont_Rep_cfun2: "cont (\<lambda>x. f\<cdot>x)" |
198 apply (cut_tac x=f in Rep_cfun) |
198 apply (cut_tac x=f in Rep_cfun) |
199 apply (simp add: cfun_def) |
199 apply (simp add: cfun_def) |
200 done |
200 done |