equal
deleted
inserted
replaced
27 apply (simp add: Abs_lift_strict) |
27 apply (simp add: Abs_lift_strict) |
28 apply (case_tac x) |
28 apply (case_tac x) |
29 apply (simp add: Def_def) |
29 apply (simp add: Def_def) |
30 done |
30 done |
31 |
31 |
32 rep_datatype "\<bottom>\<Colon>'a lift" Def |
32 old_rep_datatype "\<bottom>\<Colon>'a lift" Def |
33 by (erule lift_induct) (simp_all add: Def_def Abs_lift_inject inst_lift_pcpo) |
33 by (erule lift_induct) (simp_all add: Def_def Abs_lift_inject inst_lift_pcpo) |
34 |
34 |
35 text {* @{term bottom} and @{term Def} *} |
35 text {* @{term bottom} and @{term Def} *} |
36 |
36 |
37 lemma not_Undef_is_Def: "(x \<noteq> \<bottom>) = (\<exists>y. x = Def y)" |
37 lemma not_Undef_is_Def: "(x \<noteq> \<bottom>) = (\<exists>y. x = Def y)" |