src/HOLCF/Up.thy
changeset 27310 d0229bc6c461
parent 26962 c8b20f615d6c
child 27413 3154f3765cc7
     1.1 --- a/src/HOLCF/Up.thy	Fri Jun 20 22:51:50 2008 +0200
     1.2 +++ b/src/HOLCF/Up.thy	Fri Jun 20 23:01:09 2008 +0200
     1.3 @@ -320,7 +320,7 @@
     1.4  
     1.5  instance proof
     1.6    fix i :: nat and x :: "'a u"
     1.7 -  show "chain (\<lambda>i. approx i\<cdot>x)"
     1.8 +  show "chain (approx :: nat \<Rightarrow> 'a u \<rightarrow> 'a u)"
     1.9      unfolding approx_up_def by simp
    1.10    show "(\<Squnion>i. approx i\<cdot>x) = x"
    1.11      unfolding approx_up_def
    1.12 @@ -331,7 +331,7 @@
    1.13    have "{x::'a u. approx i\<cdot>x = x} \<subseteq>
    1.14          insert \<bottom> ((\<lambda>x. up\<cdot>x) ` {x::'a. approx i\<cdot>x = x})"
    1.15      unfolding approx_up_def
    1.16 -    by (rule subsetI, rule_tac p=x in upE, simp_all)
    1.17 +    by (rule subsetI, case_tac x, simp_all)
    1.18    thus "finite {x::'a u. approx i\<cdot>x = x}"
    1.19      by (rule finite_subset, simp add: finite_fixes_approx)
    1.20  qed