changeset 40012 | f13341a45407 |
parent 40002 | c5b5f7a3a3b1 |
child 40086 | c339c0e8fdfb |
--- a/src/HOLCF/Bifinite.thy Wed Oct 13 10:56:42 2010 -0700 +++ b/src/HOLCF/Bifinite.thy Thu Oct 14 09:28:05 2010 -0700 @@ -440,7 +440,7 @@ lemma finite_deflation_lift_approx: "finite_deflation (lift_approx i)" proof - fix x + fix x :: "'a lift" show "lift_approx i\<cdot>x \<sqsubseteq> x" unfolding lift_approx_def by (cases x, simp, simp)