changed to work with new contlubE rule

--- a/src/HOLCF/Adm.thy	Fri Jun 03 23:14:09 2005 +0200
+++ b/src/HOLCF/Adm.thy	Fri Jun 03 23:15:16 2005 +0200
@@ -79,9 +79,9 @@
 apply assumption
 apply (frule_tac f = "v" in cont2mono [THEN ch2ch_monofun])
 apply assumption
-apply (erule cont2contlub [THEN contlubE, THEN spec, THEN mp, THEN ssubst])
+apply (erule cont2contlub [THEN contlubE, THEN ssubst])
 apply assumption
-apply (erule cont2contlub [THEN contlubE, THEN spec, THEN mp, THEN ssubst])
+apply (erule cont2contlub [THEN contlubE, THEN ssubst])
 apply assumption
 apply (blast intro: lub_mono)
 done
@@ -113,7 +113,7 @@
 
 lemma adm_subst: "[|cont t; adm P|] ==> adm(%x. P (t x))"
 apply (rule admI)
-apply (simplesubst cont2contlub [THEN contlubE, THEN spec, THEN mp])
+apply (simplesubst cont2contlub [THEN contlubE])
 apply assumption
 apply assumption
 apply (erule admD)
@@ -133,7 +133,7 @@
 apply (rule chain_UU_I [THEN spec])
 apply (erule cont2mono [THEN ch2ch_monofun])
 apply assumption
-apply (erule cont2contlub [THEN contlubE, THEN spec, THEN mp, THEN subst])
+apply (erule cont2contlub [THEN contlubE, THEN subst])
 apply assumption
 apply assumption
 done