src/HOL/HOLCF/Lift.thy
changeset 55642 63beb38e9258
parent 55417 01fbfb60c33e
child 58306 117ba6cbe414
     1.1 --- a/src/HOL/HOLCF/Lift.thy	Fri Feb 21 00:09:55 2014 +0100
     1.2 +++ b/src/HOL/HOLCF/Lift.thy	Fri Feb 21 00:09:56 2014 +0100
     1.3 @@ -74,7 +74,7 @@
     1.4  subsection {* Continuity of @{const case_lift} *}
     1.5  
     1.6  lemma case_lift_eq: "case_lift \<bottom> f x = fup\<cdot>(\<Lambda> y. f (undiscr y))\<cdot>(Rep_lift x)"
     1.7 -apply (induct x, unfold lift.cases)
     1.8 +apply (induct x, unfold lift.case)
     1.9  apply (simp add: Rep_lift_strict)
    1.10  apply (simp add: Def_def Abs_lift_inverse)
    1.11  done