# HG changeset patch
# User huffman
# Date 1287666198 25200
# Node ID f4be971c574648535615d0aa922c287849bb4d97
# Parent  748911a00a5141a6a7a51347c84e60190679d764
pcpodef (open) 'a lift

diff -r 748911a00a51 -r f4be971c5746 src/HOLCF/Lift.thy
--- a/src/HOLCF/Lift.thy	Thu Oct 21 05:44:38 2010 -0700
+++ b/src/HOLCF/Lift.thy	Thu Oct 21 06:03:18 2010 -0700
@@ -10,7 +10,7 @@
 
 default_sort type
 
-pcpodef 'a lift = "UNIV :: 'a discr u set"
+pcpodef (open) 'a lift = "UNIV :: 'a discr u set"
 by simp_all
 
 instance lift :: (finite) finite_po
@@ -33,7 +33,7 @@
 done
 
 rep_datatype "\<bottom>\<Colon>'a lift" Def
-  by (erule lift_induct) (simp_all add: Def_def Abs_lift_inject lift_def inst_lift_pcpo)
+  by (erule lift_induct) (simp_all add: Def_def Abs_lift_inject inst_lift_pcpo)
 
 lemmas lift_distinct1 = lift.distinct(1)
 lemmas lift_distinct2 = lift.distinct(2)
@@ -65,7 +65,7 @@
   by simp
 
 lemma Def_below_Def: "Def x \<sqsubseteq> Def y \<longleftrightarrow> x = y"
-by (simp add: below_lift_def Def_def Abs_lift_inverse lift_def)
+by (simp add: below_lift_def Def_def Abs_lift_inverse)
 
 lemma Def_below_iff [simp]: "Def x \<sqsubseteq> y \<longleftrightarrow> Def x = y"
 by (induct y, simp, simp add: Def_below_Def)