# HG changeset patch
# User huffman
# Date 1117833316 -7200
# Node ID d67baef02f78d50aefc49e0f73a5ccf66259ba42
# Parent  91fad2051da5e8d0da7c317b09b153e9d92d00d7
changed to work with new contlubE rule

diff -r 91fad2051da5 -r d67baef02f78 src/HOLCF/Adm.thy
--- 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