--- a/src/HOLCF/Adm.thy Thu Jul 07 18:19:20 2005 +0200
+++ b/src/HOLCF/Adm.thy Thu Jul 07 18:20:08 2005 +0200
@@ -65,10 +65,10 @@
lemma adm_less: "\<lbrakk>cont u; cont v\<rbrakk> \<Longrightarrow> adm (\<lambda>x. u x \<sqsubseteq> v x)"
apply (rule admI)
-apply (simp add: cont2contlub [THEN contlubE])
+apply (simp add: cont2contlubE)
apply (rule lub_mono)
-apply (erule (1) cont2mono [THEN ch2ch_monofun])
-apply (erule (1) cont2mono [THEN ch2ch_monofun])
+apply (erule (1) ch2ch_cont)
+apply (erule (1) ch2ch_cont)
apply assumption
done
@@ -95,9 +95,9 @@
lemma adm_subst: "\<lbrakk>cont t; adm P\<rbrakk> \<Longrightarrow> adm (\<lambda>x. P (t x))"
apply (rule admI)
-apply (simp add: cont2contlub [THEN contlubE])
+apply (simp add: cont2contlubE)
apply (erule admD)
-apply (erule (1) cont2mono [THEN ch2ch_monofun])
+apply (erule (1) ch2ch_cont)
apply assumption
done
@@ -243,4 +243,3 @@
*}
end
-
--- a/src/HOLCF/Pcpodef.thy Thu Jul 07 18:19:20 2005 +0200
+++ b/src/HOLCF/Pcpodef.thy Thu Jul 07 18:20:08 2005 +0200
@@ -131,9 +131,9 @@
apply (rule monofun_fun_arg [OF cont2mono [OF cont_f]])
apply (erule is_ub_thelub)
apply (simp only: less type_definition.Abs_inverse [OF type f_in_A])
- apply (simp only: contlubE [OF cont2contlub [OF cont_f]])
+ apply (simp only: cont2contlubE [OF cont_f])
apply (rule is_lub_thelub)
- apply (erule ch2ch_monofun [OF cont2mono [OF cont_f]])
+ apply (erule ch2ch_cont [OF cont_f])
apply (rule ub_rangeI)
apply (drule_tac i=i in ub_rangeD)
apply (simp only: less type_definition.Abs_inverse [OF type f_in_A])