src/HOL/HOLCF/Lift.thy
changeset 41430 1aa23e9f2c87
parent 40834 a1249aeff5b6
child 42151 4da4fc77664b
     1.1 --- a/src/HOL/HOLCF/Lift.thy	Tue Jan 04 15:03:27 2011 -0800
     1.2 +++ b/src/HOL/HOLCF/Lift.thy	Tue Jan 04 15:32:56 2011 -0800
     1.3 @@ -32,13 +32,7 @@
     1.4  rep_datatype "\<bottom>\<Colon>'a lift" Def
     1.5    by (erule lift_induct) (simp_all add: Def_def Abs_lift_inject inst_lift_pcpo)
     1.6  
     1.7 -lemmas lift_distinct1 = lift.distinct(1)
     1.8 -lemmas lift_distinct2 = lift.distinct(2)
     1.9 -lemmas Def_not_UU = lift.distinct(2)
    1.10 -lemmas Def_inject = lift.inject
    1.11 -
    1.12 -
    1.13 -text {* @{term UU} and @{term Def} *}
    1.14 +text {* @{term bottom} and @{term Def} *}
    1.15  
    1.16  lemma not_Undef_is_Def: "(x \<noteq> \<bottom>) = (\<exists>y. x = Def y)"
    1.17    by (cases x) simp_all
    1.18 @@ -47,7 +41,7 @@
    1.19    by (cases x) simp_all
    1.20  
    1.21  text {*
    1.22 -  For @{term "x ~= UU"} in assumptions @{text defined} replaces @{text
    1.23 +  For @{term "x ~= \<bottom>"} in assumptions @{text defined} replaces @{text
    1.24    x} by @{text "Def a"} in conclusion. *}
    1.25  
    1.26  method_setup defined = {*