src/HOL/HOLCF/Lift.thy
changeset 58306 117ba6cbe414
parent 55642 63beb38e9258
child 58880 0baae4311a9f
     1.1 --- a/src/HOL/HOLCF/Lift.thy	Thu Sep 11 18:54:36 2014 +0200
     1.2 +++ b/src/HOL/HOLCF/Lift.thy	Thu Sep 11 18:54:36 2014 +0200
     1.3 @@ -29,7 +29,7 @@
     1.4  apply (simp add: Def_def)
     1.5  done
     1.6  
     1.7 -rep_datatype "\<bottom>\<Colon>'a lift" Def
     1.8 +old_rep_datatype "\<bottom>\<Colon>'a lift" Def
     1.9    by (erule lift_induct) (simp_all add: Def_def Abs_lift_inject inst_lift_pcpo)
    1.10  
    1.11  text {* @{term bottom} and @{term Def} *}