--- a/src/HOLCF/Domain.thy Fri Jul 08 02:41:19 2005 +0200
+++ b/src/HOLCF/Domain.thy Fri Jul 08 02:41:35 2005 +0200
@@ -87,7 +87,7 @@
lemma ex_up_defined_iff:
"(\<exists>x. P x \<and> x \<noteq> \<bottom>) = (\<exists>x. P (up\<cdot>x))"
apply safe
- apply (rule_tac p=x in upE1)
+ apply (rule_tac p=x in upE)
apply simp
apply fast
apply (force intro!: up_defined)
@@ -109,7 +109,7 @@
apply safe
apply (rule_tac p=y in sprodE)
apply simp
- apply (rule_tac p=x in upE1)
+ apply (rule_tac p=x in upE)
apply simp
apply fast
apply (force intro!: spair_defined)
--- a/src/HOLCF/Fixrec.thy Fri Jul 08 02:41:19 2005 +0200
+++ b/src/HOLCF/Fixrec.thy Fri Jul 08 02:41:35 2005 +0200
@@ -26,7 +26,7 @@
apply (unfold fail_def return_def)
apply (rule_tac p=p in ssumE, simp)
apply (rule_tac p=x in oneE, simp, simp)
-apply (rule_tac p=y in upE1, simp, simp)
+apply (rule_tac p=y in upE, simp, simp)
done
subsection {* Monadic bind operator *}