renamed upE1 to upE
authorhuffman
Fri Jul 08 02:41:35 2005 +0200 (2005-07-08)
changeset 167541b979f8b7e8e
parent 16753 fb6801c926d2
child 16755 fd02f9d06e43
renamed upE1 to upE
src/HOLCF/Domain.thy
src/HOLCF/Fixrec.thy
     1.1 --- a/src/HOLCF/Domain.thy	Fri Jul 08 02:41:19 2005 +0200
     1.2 +++ b/src/HOLCF/Domain.thy	Fri Jul 08 02:41:35 2005 +0200
     1.3 @@ -87,7 +87,7 @@
     1.4  lemma ex_up_defined_iff:
     1.5    "(\<exists>x. P x \<and> x \<noteq> \<bottom>) = (\<exists>x. P (up\<cdot>x))"
     1.6   apply safe
     1.7 -  apply (rule_tac p=x in upE1)
     1.8 +  apply (rule_tac p=x in upE)
     1.9     apply simp
    1.10    apply fast
    1.11   apply (force intro!: up_defined)
    1.12 @@ -109,7 +109,7 @@
    1.13   apply safe
    1.14    apply (rule_tac p=y in sprodE)
    1.15     apply simp
    1.16 -  apply (rule_tac p=x in upE1)
    1.17 +  apply (rule_tac p=x in upE)
    1.18     apply simp
    1.19    apply fast
    1.20   apply (force intro!: spair_defined)
     2.1 --- a/src/HOLCF/Fixrec.thy	Fri Jul 08 02:41:19 2005 +0200
     2.2 +++ b/src/HOLCF/Fixrec.thy	Fri Jul 08 02:41:35 2005 +0200
     2.3 @@ -26,7 +26,7 @@
     2.4  apply (unfold fail_def return_def)
     2.5  apply (rule_tac p=p in ssumE, simp)
     2.6  apply (rule_tac p=x in oneE, simp, simp)
     2.7 -apply (rule_tac p=y in upE1, simp, simp)
     2.8 +apply (rule_tac p=y in upE, simp, simp)
     2.9  done
    2.10  
    2.11  subsection {* Monadic bind operator *}