src/HOLCF/Lift.thy

 pcpodef 'a lift = "UNIV :: 'a discr u set"
 by simp
 
 lemmas inst_lift_pcpo = Abs_lift_strict [symmetric]
 
-constdefs
-  Def :: "'a \<Rightarrow> 'a lift"
-  "Def x \<equiv> Abs_lift (up\<cdot>(Discr x))"
+definition
+  Def :: "'a \<Rightarrow> 'a lift" where
+  "Def x = Abs_lift (up\<cdot>(Discr x))"
 
 subsection {* Lift as a datatype *}
 
 lemma lift_distinct1: "\<bottom> \<noteq> Def x"
 by (simp add: Def_def Abs_lift_inject lift_def inst_lift_pcpo)

 lemma cont_Rep_CFun_app_app: "\<lbrakk>cont g; cont f\<rbrakk> \<Longrightarrow> cont(\<lambda>x. ((f x)\<cdot>(g x)) s t)"
 by (rule cont_Rep_CFun_app [THEN cont2cont_fun])
 
 subsection {* Further operations *}
 
-constdefs
-  flift1 :: "('a \<Rightarrow> 'b::pcpo) \<Rightarrow> ('a lift \<rightarrow> 'b)" (binder "FLIFT " 10)
-  "flift1 \<equiv> \<lambda>f. (\<Lambda> x. lift_case \<bottom> f x)"
-
-  flift2 :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a lift \<rightarrow> 'b lift)"
-  "flift2 f \<equiv> FLIFT x. Def (f x)"
-
-  liftpair :: "'a lift \<times> 'b lift \<Rightarrow> ('a \<times> 'b) lift"
-  "liftpair x \<equiv> csplit\<cdot>(FLIFT x y. Def (x, y))\<cdot>x"
+definition
+  flift1 :: "('a \<Rightarrow> 'b::pcpo) \<Rightarrow> ('a lift \<rightarrow> 'b)"  (binder "FLIFT " 10)  where
+  "flift1 = (\<lambda>f. (\<Lambda> x. lift_case \<bottom> f x))"
+
+definition
+  flift2 :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a lift \<rightarrow> 'b lift)" where
+  "flift2 f = (FLIFT x. Def (f x))"
+
+definition
+  liftpair :: "'a lift \<times> 'b lift \<Rightarrow> ('a \<times> 'b) lift" where
+  "liftpair x = csplit\<cdot>(FLIFT x y. Def (x, y))\<cdot>x"
 
 subsection {* Continuity Proofs for flift1, flift2 *}
 
 text {* Need the instance of @{text flat}. *}