# HG changeset patch
# User huffman
# Date 1120753208 -7200
# Node ID b70bac29b11d50a74c8a3df61edd3568c0426ea8
# Parent  f0fd06dc93e39bd76b306a7f6b6cbef103c2aa7e
use theorems ch2ch_cont, cont2contlubE

diff -r f0fd06dc93e3 -r b70bac29b11d src/HOLCF/Adm.thy
--- 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
-
diff -r f0fd06dc93e3 -r b70bac29b11d src/HOLCF/Pcpodef.thy
--- 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])