src/HOLCF/Up.thy
changeset 16553 aa36d41e4263
parent 16326 50a613925c4e
child 16753 fb6801c926d2
     1.1 --- a/src/HOLCF/Up.thy	Thu Jun 23 21:27:23 2005 +0200
     1.2 +++ b/src/HOLCF/Up.thy	Thu Jun 23 22:07:30 2005 +0200
     1.3 @@ -309,7 +309,7 @@
     1.4  lemma fup2 [simp]: "fup\<cdot>f\<cdot>(up\<cdot>x) = f\<cdot>x"
     1.5  by (simp add: up_def fup_def cont_Iup cont_Ifup1 cont_Ifup2 )
     1.6  
     1.7 -lemma fup3: "fup\<cdot>up\<cdot>x = x"
     1.8 +lemma fup3 [simp]: "fup\<cdot>up\<cdot>x = x"
     1.9  by (rule_tac p=x in upE1, simp_all)
    1.10  
    1.11  end