# HG changeset patch
# User huffman
# Date 1120783295 -7200
# Node ID 1b979f8b7e8e336e12f17af7aa19848161a2a9c7
# Parent  fb6801c926d2f13171ac7778e276a408031ec291
renamed upE1 to upE

diff -r fb6801c926d2 -r 1b979f8b7e8e src/HOLCF/Domain.thy
--- 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)
diff -r fb6801c926d2 -r 1b979f8b7e8e src/HOLCF/Fixrec.thy
--- 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 *}