# HG changeset patch
# User huffman
# Date 1288792929 25200
# Node ID 3b7f570723f9908e5b29662b04c508359817bd66
# Parent  73f2b99b549d6e59da4b0a8f0f4720fa0f5ac48c# Parent  abc52faa7761eabb46a4c141b7e04dd55608222a
merged

diff -r abc52faa7761 -r 3b7f570723f9 src/HOLCF/Algebraic.thy
--- a/src/HOLCF/Algebraic.thy	Wed Nov 03 10:44:53 2010 +0100
+++ b/src/HOLCF/Algebraic.thy	Wed Nov 03 07:02:09 2010 -0700
@@ -191,7 +191,7 @@
 lemma compact_cast_iff: "compact (cast\<cdot>d) \<longleftrightarrow> compact d"
 apply (rule iffI)
 apply (simp only: compact_def cast_below_cast [symmetric])
-apply (erule adm_subst [OF cont_Rep_CFun2])
+apply (erule adm_subst [OF cont_Rep_cfun2])
 apply (erule compact_cast)
 done
 
diff -r abc52faa7761 -r 3b7f570723f9 src/HOLCF/Cfun.thy
--- a/src/HOLCF/Cfun.thy	Wed Nov 03 10:44:53 2010 +0100
+++ b/src/HOLCF/Cfun.thy	Wed Nov 03 07:02:09 2010 -0700
@@ -13,28 +13,28 @@
 
 subsection {* Definition of continuous function type *}
 
-cpodef (CFun)  ('a, 'b) cfun (infixr "->" 0) = "{f::'a => 'b. cont f}"
+cpodef ('a, 'b) cfun (infixr "->" 0) = "{f::'a => 'b. cont f}"
 by (auto intro: cont_const adm_cont)
 
 type_notation (xsymbols)
   cfun  ("(_ \<rightarrow>/ _)" [1, 0] 0)
 
 notation
-  Rep_CFun  ("(_$/_)" [999,1000] 999)
+  Rep_cfun  ("(_$/_)" [999,1000] 999)
 
 notation (xsymbols)
-  Rep_CFun  ("(_\<cdot>/_)" [999,1000] 999)
+  Rep_cfun  ("(_\<cdot>/_)" [999,1000] 999)
 
 notation (HTML output)
-  Rep_CFun  ("(_\<cdot>/_)" [999,1000] 999)
+  Rep_cfun  ("(_\<cdot>/_)" [999,1000] 999)
 
 subsection {* Syntax for continuous lambda abstraction *}
 
 syntax "_cabs" :: "'a"
 
 parse_translation {*
-(* rewrite (_cabs x t) => (Abs_CFun (%x. t)) *)
-  [mk_binder_tr (@{syntax_const "_cabs"}, @{const_syntax Abs_CFun})];
+(* rewrite (_cabs x t) => (Abs_cfun (%x. t)) *)
+  [mk_binder_tr (@{syntax_const "_cabs"}, @{const_syntax Abs_cfun})];
 *}
 
 text {* To avoid eta-contraction of body: *}
@@ -50,7 +50,7 @@
           val (x,t') = atomic_abs_tr' abs';
         in Syntax.const @{syntax_const "_cabs"} $ x $ t' end;
 
-  in [(@{const_syntax Abs_CFun}, cabs_tr')] end;
+  in [(@{const_syntax Abs_cfun}, cabs_tr')] end;
 *}
 
 text {* Syntax for nested abstractions *}
@@ -88,32 +88,32 @@
 
 text {* Dummy patterns for continuous abstraction *}
 translations
-  "\<Lambda> _. t" => "CONST Abs_CFun (\<lambda> _. t)"
+  "\<Lambda> _. t" => "CONST Abs_cfun (\<lambda> _. t)"
 
 subsection {* Continuous function space is pointed *}
 
-lemma UU_CFun: "\<bottom> \<in> CFun"
-by (simp add: CFun_def inst_fun_pcpo)
+lemma UU_cfun: "\<bottom> \<in> cfun"
+by (simp add: cfun_def inst_fun_pcpo)
 
 instance cfun :: (cpo, discrete_cpo) discrete_cpo
-by intro_classes (simp add: below_CFun_def Rep_CFun_inject)
+by intro_classes (simp add: below_cfun_def Rep_cfun_inject)
 
 instance cfun :: (cpo, pcpo) pcpo
-by (rule typedef_pcpo [OF type_definition_CFun below_CFun_def UU_CFun])
+by (rule typedef_pcpo [OF type_definition_cfun below_cfun_def UU_cfun])
 
-lemmas Rep_CFun_strict =
-  typedef_Rep_strict [OF type_definition_CFun below_CFun_def UU_CFun]
+lemmas Rep_cfun_strict =
+  typedef_Rep_strict [OF type_definition_cfun below_cfun_def UU_cfun]
 
-lemmas Abs_CFun_strict =
-  typedef_Abs_strict [OF type_definition_CFun below_CFun_def UU_CFun]
+lemmas Abs_cfun_strict =
+  typedef_Abs_strict [OF type_definition_cfun below_cfun_def UU_cfun]
 
 text {* function application is strict in its first argument *}
 
-lemma Rep_CFun_strict1 [simp]: "\<bottom>\<cdot>x = \<bottom>"
-by (simp add: Rep_CFun_strict)
+lemma Rep_cfun_strict1 [simp]: "\<bottom>\<cdot>x = \<bottom>"
+by (simp add: Rep_cfun_strict)
 
 lemma LAM_strict [simp]: "(\<Lambda> x. \<bottom>) = \<bottom>"
-by (simp add: inst_fun_pcpo [symmetric] Abs_CFun_strict)
+by (simp add: inst_fun_pcpo [symmetric] Abs_cfun_strict)
 
 text {* for compatibility with old HOLCF-Version *}
 lemma inst_cfun_pcpo: "\<bottom> = (\<Lambda> x. \<bottom>)"
@@ -123,11 +123,11 @@
 
 text {* Beta-equality for continuous functions *}
 
-lemma Abs_CFun_inverse2: "cont f \<Longrightarrow> Rep_CFun (Abs_CFun f) = f"
-by (simp add: Abs_CFun_inverse CFun_def)
+lemma Abs_cfun_inverse2: "cont f \<Longrightarrow> Rep_cfun (Abs_cfun f) = f"
+by (simp add: Abs_cfun_inverse cfun_def)
 
 lemma beta_cfun: "cont f \<Longrightarrow> (\<Lambda> x. f x)\<cdot>u = f u"
-by (simp add: Abs_CFun_inverse2)
+by (simp add: Abs_cfun_inverse2)
 
 text {* Beta-reduction simproc *}
 
@@ -144,7 +144,7 @@
   that would otherwise be caused by large continuity side conditions.
 *}
 
-simproc_setup beta_cfun_proc ("Abs_CFun f\<cdot>x") = {*
+simproc_setup beta_cfun_proc ("Abs_cfun f\<cdot>x") = {*
   fn phi => fn ss => fn ct =>
     let
       val dest = Thm.dest_comb;
@@ -160,12 +160,12 @@
 text {* Eta-equality for continuous functions *}
 
 lemma eta_cfun: "(\<Lambda> x. f\<cdot>x) = f"
-by (rule Rep_CFun_inverse)
+by (rule Rep_cfun_inverse)
 
 text {* Extensionality for continuous functions *}
 
 lemma cfun_eq_iff: "f = g \<longleftrightarrow> (\<forall>x. f\<cdot>x = g\<cdot>x)"
-by (simp add: Rep_CFun_inject [symmetric] fun_eq_iff)
+by (simp add: Rep_cfun_inject [symmetric] fun_eq_iff)
 
 lemma cfun_eqI: "(\<And>x. f\<cdot>x = g\<cdot>x) \<Longrightarrow> f = g"
 by (simp add: cfun_eq_iff)
@@ -173,7 +173,7 @@
 text {* Extensionality wrt. ordering for continuous functions *}
 
 lemma cfun_below_iff: "f \<sqsubseteq> g \<longleftrightarrow> (\<forall>x. f\<cdot>x \<sqsubseteq> g\<cdot>x)" 
-by (simp add: below_CFun_def fun_below_iff)
+by (simp add: below_cfun_def fun_below_iff)
 
 lemma cfun_belowI: "(\<And>x. f\<cdot>x \<sqsubseteq> g\<cdot>x) \<Longrightarrow> f \<sqsubseteq> g"
 by (simp add: cfun_below_iff)
@@ -191,32 +191,32 @@
 
 subsection {* Continuity of application *}
 
-lemma cont_Rep_CFun1: "cont (\<lambda>f. f\<cdot>x)"
-by (rule cont_Rep_CFun [THEN cont2cont_fun])
+lemma cont_Rep_cfun1: "cont (\<lambda>f. f\<cdot>x)"
+by (rule cont_Rep_cfun [THEN cont2cont_fun])
 
-lemma cont_Rep_CFun2: "cont (\<lambda>x. f\<cdot>x)"
-apply (cut_tac x=f in Rep_CFun)
-apply (simp add: CFun_def)
+lemma cont_Rep_cfun2: "cont (\<lambda>x. f\<cdot>x)"
+apply (cut_tac x=f in Rep_cfun)
+apply (simp add: cfun_def)
 done
 
-lemmas monofun_Rep_CFun = cont_Rep_CFun [THEN cont2mono]
+lemmas monofun_Rep_cfun = cont_Rep_cfun [THEN cont2mono]
 
-lemmas monofun_Rep_CFun1 = cont_Rep_CFun1 [THEN cont2mono, standard]
-lemmas monofun_Rep_CFun2 = cont_Rep_CFun2 [THEN cont2mono, standard]
+lemmas monofun_Rep_cfun1 = cont_Rep_cfun1 [THEN cont2mono, standard]
+lemmas monofun_Rep_cfun2 = cont_Rep_cfun2 [THEN cont2mono, standard]
 
-text {* contlub, cont properties of @{term Rep_CFun} in each argument *}
+text {* contlub, cont properties of @{term Rep_cfun} in each argument *}
 
 lemma contlub_cfun_arg: "chain Y \<Longrightarrow> f\<cdot>(\<Squnion>i. Y i) = (\<Squnion>i. f\<cdot>(Y i))"
-by (rule cont_Rep_CFun2 [THEN cont2contlubE])
+by (rule cont_Rep_cfun2 [THEN cont2contlubE])
 
 lemma cont_cfun_arg: "chain Y \<Longrightarrow> range (\<lambda>i. f\<cdot>(Y i)) <<| f\<cdot>(\<Squnion>i. Y i)"
-by (rule cont_Rep_CFun2 [THEN contE])
+by (rule cont_Rep_cfun2 [THEN contE])
 
 lemma contlub_cfun_fun: "chain F \<Longrightarrow> (\<Squnion>i. F i)\<cdot>x = (\<Squnion>i. F i\<cdot>x)"
-by (rule cont_Rep_CFun1 [THEN cont2contlubE])
+by (rule cont_Rep_cfun1 [THEN cont2contlubE])
 
 lemma cont_cfun_fun: "chain F \<Longrightarrow> range (\<lambda>i. F i\<cdot>x) <<| (\<Squnion>i. F i)\<cdot>x"
-by (rule cont_Rep_CFun1 [THEN contE])
+by (rule cont_Rep_cfun1 [THEN contE])
 
 text {* monotonicity of application *}
 
@@ -224,7 +224,7 @@
 by (simp add: cfun_below_iff)
 
 lemma monofun_cfun_arg: "x \<sqsubseteq> y \<Longrightarrow> f\<cdot>x \<sqsubseteq> f\<cdot>y"
-by (rule monofun_Rep_CFun2 [THEN monofunE])
+by (rule monofun_Rep_cfun2 [THEN monofunE])
 
 lemma monofun_cfun: "\<lbrakk>f \<sqsubseteq> g; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> f\<cdot>x \<sqsubseteq> g\<cdot>y"
 by (rule below_trans [OF monofun_cfun_fun monofun_cfun_arg])
@@ -232,15 +232,15 @@
 text {* ch2ch - rules for the type @{typ "'a -> 'b"} *}
 
 lemma chain_monofun: "chain Y \<Longrightarrow> chain (\<lambda>i. f\<cdot>(Y i))"
-by (erule monofun_Rep_CFun2 [THEN ch2ch_monofun])
+by (erule monofun_Rep_cfun2 [THEN ch2ch_monofun])
 
-lemma ch2ch_Rep_CFunR: "chain Y \<Longrightarrow> chain (\<lambda>i. f\<cdot>(Y i))"
-by (rule monofun_Rep_CFun2 [THEN ch2ch_monofun])
+lemma ch2ch_Rep_cfunR: "chain Y \<Longrightarrow> chain (\<lambda>i. f\<cdot>(Y i))"
+by (rule monofun_Rep_cfun2 [THEN ch2ch_monofun])
 
-lemma ch2ch_Rep_CFunL: "chain F \<Longrightarrow> chain (\<lambda>i. (F i)\<cdot>x)"
-by (rule monofun_Rep_CFun1 [THEN ch2ch_monofun])
+lemma ch2ch_Rep_cfunL: "chain F \<Longrightarrow> chain (\<lambda>i. (F i)\<cdot>x)"
+by (rule monofun_Rep_cfun1 [THEN ch2ch_monofun])
 
-lemma ch2ch_Rep_CFun [simp]:
+lemma ch2ch_Rep_cfun [simp]:
   "\<lbrakk>chain F; chain Y\<rbrakk> \<Longrightarrow> chain (\<lambda>i. (F i)\<cdot>(Y i))"
 by (simp add: chain_def monofun_cfun)
 
@@ -248,7 +248,7 @@
   "\<lbrakk>\<And>x. chain (\<lambda>i. S i x); \<And>i. cont (\<lambda>x. S i x)\<rbrakk> \<Longrightarrow> chain (\<lambda>i. \<Lambda> x. S i x)"
 by (simp add: chain_def cfun_below_iff)
 
-text {* contlub, cont properties of @{term Rep_CFun} in both arguments *}
+text {* contlub, cont properties of @{term Rep_cfun} in both arguments *}
 
 lemma contlub_cfun: 
   "\<lbrakk>chain F; chain Y\<rbrakk> \<Longrightarrow> (\<Squnion>i. F i)\<cdot>(\<Squnion>i. Y i) = (\<Squnion>i. F i\<cdot>(Y i))"
@@ -257,15 +257,15 @@
 lemma cont_cfun: 
   "\<lbrakk>chain F; chain Y\<rbrakk> \<Longrightarrow> range (\<lambda>i. F i\<cdot>(Y i)) <<| (\<Squnion>i. F i)\<cdot>(\<Squnion>i. Y i)"
 apply (rule thelubE)
-apply (simp only: ch2ch_Rep_CFun)
+apply (simp only: ch2ch_Rep_cfun)
 apply (simp only: contlub_cfun)
 done
 
 lemma contlub_LAM:
   "\<lbrakk>\<And>x. chain (\<lambda>i. F i x); \<And>i. cont (\<lambda>x. F i x)\<rbrakk>
     \<Longrightarrow> (\<Lambda> x. \<Squnion>i. F i x) = (\<Squnion>i. \<Lambda> x. F i x)"
-apply (simp add: thelub_CFun)
-apply (simp add: Abs_CFun_inverse2)
+apply (simp add: thelub_cfun)
+apply (simp add: Abs_cfun_inverse2)
 apply (simp add: thelub_fun ch2ch_lambda)
 done
 
@@ -291,17 +291,17 @@
 
 subsection {* Continuity simplification procedure *}
 
-text {* cont2cont lemma for @{term Rep_CFun} *}
+text {* cont2cont lemma for @{term Rep_cfun} *}
 
-lemma cont2cont_Rep_CFun [simp, cont2cont]:
+lemma cont2cont_APP [simp, cont2cont]:
   assumes f: "cont (\<lambda>x. f x)"
   assumes t: "cont (\<lambda>x. t x)"
   shows "cont (\<lambda>x. (f x)\<cdot>(t x))"
 proof -
   have 1: "\<And>y. cont (\<lambda>x. (f x)\<cdot>y)"
-    using cont_Rep_CFun1 f by (rule cont_compose)
+    using cont_Rep_cfun1 f by (rule cont_compose)
   show "cont (\<lambda>x. (f x)\<cdot>(t x))"
-    using t cont_Rep_CFun2 1 by (rule cont_apply)
+    using t cont_Rep_cfun2 1 by (rule cont_apply)
 qed
 
 text {*
@@ -309,11 +309,11 @@
   These lemmas are needed in theories that use types like @{typ "'a \<rightarrow> 'b \<Rightarrow> 'c"}.
 *}
 
-lemma cont_Rep_CFun_app [simp]: "\<lbrakk>cont f; cont g\<rbrakk> \<Longrightarrow> cont (\<lambda>x. ((f x)\<cdot>(g x)) s)"
-by (rule cont2cont_Rep_CFun [THEN cont2cont_fun])
+lemma cont_APP_app [simp]: "\<lbrakk>cont f; cont g\<rbrakk> \<Longrightarrow> cont (\<lambda>x. ((f x)\<cdot>(g x)) s)"
+by (rule cont2cont_APP [THEN cont2cont_fun])
 
-lemma cont_Rep_CFun_app_app [simp]: "\<lbrakk>cont f; cont g\<rbrakk> \<Longrightarrow> cont (\<lambda>x. ((f x)\<cdot>(g x)) s t)"
-by (rule cont_Rep_CFun_app [THEN cont2cont_fun])
+lemma cont_APP_app_app [simp]: "\<lbrakk>cont f; cont g\<rbrakk> \<Longrightarrow> cont (\<lambda>x. ((f x)\<cdot>(g x)) s t)"
+by (rule cont_APP_app [THEN cont2cont_fun])
 
 
 text {* cont2mono Lemma for @{term "%x. LAM y. c1(x)(y)"} *}
@@ -334,9 +334,9 @@
   assumes f1: "\<And>x. cont (\<lambda>y. f x y)"
   assumes f2: "\<And>y. cont (\<lambda>x. f x y)"
   shows "cont (\<lambda>x. \<Lambda> y. f x y)"
-proof (rule cont_Abs_CFun)
+proof (rule cont_Abs_cfun)
   fix x
-  from f1 show "f x \<in> CFun" by (simp add: CFun_def)
+  from f1 show "f x \<in> cfun" by (simp add: cfun_def)
   from f2 show "cont f" by (rule cont2cont_lambda)
 qed
 
@@ -356,24 +356,24 @@
 by (simp add: cont2cont_LAM)
 
 lemmas cont_lemmas1 =
-  cont_const cont_id cont_Rep_CFun2 cont2cont_Rep_CFun cont2cont_LAM
+  cont_const cont_id cont_Rep_cfun2 cont2cont_APP cont2cont_LAM
 
 subsection {* Miscellaneous *}
 
-text {* Monotonicity of @{term Abs_CFun} *}
+text {* Monotonicity of @{term Abs_cfun} *}
 
-lemma semi_monofun_Abs_CFun:
-  "\<lbrakk>cont f; cont g; f \<sqsubseteq> g\<rbrakk> \<Longrightarrow> Abs_CFun f \<sqsubseteq> Abs_CFun g"
-by (simp add: below_CFun_def Abs_CFun_inverse2)
+lemma semi_monofun_Abs_cfun:
+  "\<lbrakk>cont f; cont g; f \<sqsubseteq> g\<rbrakk> \<Longrightarrow> Abs_cfun f \<sqsubseteq> Abs_cfun g"
+by (simp add: below_cfun_def Abs_cfun_inverse2)
 
 text {* some lemmata for functions with flat/chfin domain/range types *}
 
-lemma chfin_Rep_CFunR: "chain (Y::nat => 'a::cpo->'b::chfin)  
+lemma chfin_Rep_cfunR: "chain (Y::nat => 'a::cpo->'b::chfin)  
       ==> !s. ? n. (LUB i. Y i)$s = Y n$s"
 apply (rule allI)
 apply (subst contlub_cfun_fun)
 apply assumption
-apply (fast intro!: thelubI chfin lub_finch2 chfin2finch ch2ch_Rep_CFunL)
+apply (fast intro!: thelubI chfin lub_finch2 chfin2finch ch2ch_Rep_cfunL)
 done
 
 lemma adm_chfindom: "adm (\<lambda>(u::'a::cpo \<rightarrow> 'b::chfin). P(u\<cdot>s))"
diff -r abc52faa7761 -r 3b7f570723f9 src/HOLCF/ConvexPD.thy
--- a/src/HOLCF/ConvexPD.thy	Wed Nov 03 10:44:53 2010 +0100
+++ b/src/HOLCF/ConvexPD.thy	Wed Nov 03 07:02:09 2010 -0700
@@ -256,7 +256,7 @@
 using convex_unit_Rep_compact_basis [of compact_bot]
 by (simp add: inst_convex_pd_pcpo)
 
-lemma convex_unit_strict_iff [simp]: "{x}\<natural> = \<bottom> \<longleftrightarrow> x = \<bottom>"
+lemma convex_unit_bottom_iff [simp]: "{x}\<natural> = \<bottom> \<longleftrightarrow> x = \<bottom>"
 unfolding convex_unit_strict [symmetric] by (rule convex_unit_eq_iff)
 
 lemma compact_convex_unit: "compact x \<Longrightarrow> compact {x}\<natural>"
@@ -265,7 +265,7 @@
 lemma compact_convex_unit_iff [simp]: "compact {x}\<natural> \<longleftrightarrow> compact x"
 apply (safe elim!: compact_convex_unit)
 apply (simp only: compact_def convex_unit_below_iff [symmetric])
-apply (erule adm_subst [OF cont_Rep_CFun2])
+apply (erule adm_subst [OF cont_Rep_cfun2])
 done
 
 lemma compact_convex_plus [simp]:
diff -r abc52faa7761 -r 3b7f570723f9 src/HOLCF/Deflation.thy
--- a/src/HOLCF/Deflation.thy	Wed Nov 03 10:44:53 2010 +0100
+++ b/src/HOLCF/Deflation.thy	Wed Nov 03 07:02:09 2010 -0700
@@ -207,7 +207,7 @@
 proof -
   assume "compact (e\<cdot>x)"
   hence "adm (\<lambda>y. \<not> e\<cdot>x \<sqsubseteq> y)" by (rule compactD)
-  hence "adm (\<lambda>y. \<not> e\<cdot>x \<sqsubseteq> e\<cdot>y)" by (rule adm_subst [OF cont_Rep_CFun2])
+  hence "adm (\<lambda>y. \<not> e\<cdot>x \<sqsubseteq> e\<cdot>y)" by (rule adm_subst [OF cont_Rep_cfun2])
   hence "adm (\<lambda>y. \<not> x \<sqsubseteq> y)" by simp
   thus "compact x" by (rule compactI)
 qed
@@ -216,7 +216,7 @@
 proof -
   assume "compact x"
   hence "adm (\<lambda>y. \<not> x \<sqsubseteq> y)" by (rule compactD)
-  hence "adm (\<lambda>y. \<not> x \<sqsubseteq> p\<cdot>y)" by (rule adm_subst [OF cont_Rep_CFun2])
+  hence "adm (\<lambda>y. \<not> x \<sqsubseteq> p\<cdot>y)" by (rule adm_subst [OF cont_Rep_cfun2])
   hence "adm (\<lambda>y. \<not> e\<cdot>x \<sqsubseteq> y)" by (simp add: e_below_iff_below_p)
   thus "compact (e\<cdot>x)" by (rule compactI)
 qed
@@ -392,7 +392,7 @@
   finally show "e\<cdot>\<bottom> = \<bottom>" by simp
 qed
 
-lemma e_defined_iff [simp]: "e\<cdot>x = \<bottom> \<longleftrightarrow> x = \<bottom>"
+lemma e_bottom_iff [simp]: "e\<cdot>x = \<bottom> \<longleftrightarrow> x = \<bottom>"
 by (rule e_eq_iff [where y="\<bottom>", unfolded e_strict])
 
 lemma e_defined: "x \<noteq> \<bottom> \<Longrightarrow> e\<cdot>x \<noteq> \<bottom>"
diff -r abc52faa7761 -r 3b7f570723f9 src/HOLCF/Domain.thy
--- a/src/HOLCF/Domain.thy	Wed Nov 03 10:44:53 2010 +0100
+++ b/src/HOLCF/Domain.thy	Wed Nov 03 07:02:09 2010 -0700
@@ -22,25 +22,25 @@
 
 text {* Lemmas for proving nchotomy rule: *}
 
-lemma ex_one_defined_iff:
+lemma ex_one_bottom_iff:
   "(\<exists>x. P x \<and> x \<noteq> \<bottom>) = P ONE"
 by simp
 
-lemma ex_up_defined_iff:
+lemma ex_up_bottom_iff:
   "(\<exists>x. P x \<and> x \<noteq> \<bottom>) = (\<exists>x. P (up\<cdot>x))"
 by (safe, case_tac x, auto)
 
-lemma ex_sprod_defined_iff:
+lemma ex_sprod_bottom_iff:
  "(\<exists>y. P y \<and> y \<noteq> \<bottom>) =
   (\<exists>x y. (P (:x, y:) \<and> x \<noteq> \<bottom>) \<and> y \<noteq> \<bottom>)"
 by (safe, case_tac y, auto)
 
-lemma ex_sprod_up_defined_iff:
+lemma ex_sprod_up_bottom_iff:
  "(\<exists>y. P y \<and> y \<noteq> \<bottom>) =
   (\<exists>x y. P (:up\<cdot>x, y:) \<and> y \<noteq> \<bottom>)"
 by (safe, case_tac y, simp, case_tac x, auto)
 
-lemma ex_ssum_defined_iff:
+lemma ex_ssum_bottom_iff:
  "(\<exists>x. P x \<and> x \<noteq> \<bottom>) =
  ((\<exists>x. P (sinl\<cdot>x) \<and> x \<noteq> \<bottom>) \<or>
   (\<exists>x. P (sinr\<cdot>x) \<and> x \<noteq> \<bottom>))"
@@ -49,12 +49,12 @@
 lemma exh_start: "p = \<bottom> \<or> (\<exists>x. p = x \<and> x \<noteq> \<bottom>)"
   by auto
 
-lemmas ex_defined_iffs =
-   ex_ssum_defined_iff
-   ex_sprod_up_defined_iff
-   ex_sprod_defined_iff
-   ex_up_defined_iff
-   ex_one_defined_iff
+lemmas ex_bottom_iffs =
+   ex_ssum_bottom_iff
+   ex_sprod_up_bottom_iff
+   ex_sprod_bottom_iff
+   ex_up_bottom_iff
+   ex_one_bottom_iff
 
 text {* Rules for turning nchotomy into exhaust: *}
 
@@ -78,14 +78,14 @@
 lemmas con_strict_rules =
   sinl_strict sinr_strict spair_strict1 spair_strict2
 
-lemmas con_defined_iff_rules =
-  sinl_defined_iff sinr_defined_iff spair_strict_iff up_defined ONE_defined
+lemmas con_bottom_iff_rules =
+  sinl_bottom_iff sinr_bottom_iff spair_bottom_iff up_defined ONE_defined
 
 lemmas con_below_iff_rules =
-  sinl_below sinr_below sinl_below_sinr sinr_below_sinl con_defined_iff_rules
+  sinl_below sinr_below sinl_below_sinr sinr_below_sinl con_bottom_iff_rules
 
 lemmas con_eq_iff_rules =
-  sinl_eq sinr_eq sinl_eq_sinr sinr_eq_sinl con_defined_iff_rules
+  sinl_eq sinr_eq sinl_eq_sinr sinr_eq_sinl con_bottom_iff_rules
 
 lemmas sel_strict_rules =
   cfcomp2 sscase1 sfst_strict ssnd_strict fup1
@@ -102,8 +102,8 @@
   sel_strict_rules sel_app_extra_rules
   ssnd_spair sfst_spair up_defined spair_defined
 
-lemmas sel_defined_iff_rules =
-  cfcomp2 sfst_defined_iff ssnd_defined_iff
+lemmas sel_bottom_iff_rules =
+  cfcomp2 sfst_bottom_iff ssnd_bottom_iff
 
 lemmas take_con_rules =
   ssum_map_sinl' ssum_map_sinr' sprod_map_spair' u_map_up
diff -r abc52faa7761 -r 3b7f570723f9 src/HOLCF/Domain_Aux.thy
--- a/src/HOLCF/Domain_Aux.thy	Wed Nov 03 10:44:53 2010 +0100
+++ b/src/HOLCF/Domain_Aux.thy	Wed Nov 03 07:02:09 2010 -0700
@@ -71,19 +71,19 @@
 lemma rep_defined: "z \<noteq> \<bottom> \<Longrightarrow> rep\<cdot>z \<noteq> \<bottom>"
   by (rule iso.abs_defined [OF iso.swap]) (rule iso_axioms)
 
-lemma abs_defined_iff: "(abs\<cdot>x = \<bottom>) = (x = \<bottom>)"
+lemma abs_bottom_iff: "(abs\<cdot>x = \<bottom>) = (x = \<bottom>)"
   by (auto elim: abs_defin' intro: abs_strict)
 
-lemma rep_defined_iff: "(rep\<cdot>x = \<bottom>) = (x = \<bottom>)"
-  by (rule iso.abs_defined_iff [OF iso.swap]) (rule iso_axioms)
+lemma rep_bottom_iff: "(rep\<cdot>x = \<bottom>) = (x = \<bottom>)"
+  by (rule iso.abs_bottom_iff [OF iso.swap]) (rule iso_axioms)
 
 lemma casedist_rule: "rep\<cdot>x = \<bottom> \<or> P \<Longrightarrow> x = \<bottom> \<or> P"
-  by (simp add: rep_defined_iff)
+  by (simp add: rep_bottom_iff)
 
 lemma compact_abs_rev: "compact (abs\<cdot>x) \<Longrightarrow> compact x"
 proof (unfold compact_def)
   assume "adm (\<lambda>y. \<not> abs\<cdot>x \<sqsubseteq> y)"
-  with cont_Rep_CFun2
+  with cont_Rep_cfun2
   have "adm (\<lambda>y. \<not> abs\<cdot>x \<sqsubseteq> abs\<cdot>y)" by (rule adm_subst)
   then show "adm (\<lambda>y. \<not> x \<sqsubseteq> y)" using abs_below by simp
 qed
diff -r abc52faa7761 -r 3b7f570723f9 src/HOLCF/Fix.thy
--- a/src/HOLCF/Fix.thy	Wed Nov 03 10:44:53 2010 +0100
+++ b/src/HOLCF/Fix.thy	Wed Nov 03 07:02:09 2010 -0700
@@ -119,7 +119,7 @@
 
 text {* strictness of @{term fix} *}
 
-lemma fix_defined_iff: "(fix\<cdot>F = \<bottom>) = (F\<cdot>\<bottom> = \<bottom>)"
+lemma fix_bottom_iff: "(fix\<cdot>F = \<bottom>) = (F\<cdot>\<bottom> = \<bottom>)"
 apply (rule iffI)
 apply (erule subst)
 apply (rule fix_eq [symmetric])
@@ -127,10 +127,10 @@
 done
 
 lemma fix_strict: "F\<cdot>\<bottom> = \<bottom> \<Longrightarrow> fix\<cdot>F = \<bottom>"
-by (simp add: fix_defined_iff)
+by (simp add: fix_bottom_iff)
 
 lemma fix_defined: "F\<cdot>\<bottom> \<noteq> \<bottom> \<Longrightarrow> fix\<cdot>F \<noteq> \<bottom>"
-by (simp add: fix_defined_iff)
+by (simp add: fix_bottom_iff)
 
 text {* @{term fix} applied to identity and constant functions *}
 
diff -r abc52faa7761 -r 3b7f570723f9 src/HOLCF/Fixrec.thy
--- a/src/HOLCF/Fixrec.thy	Wed Nov 03 10:44:53 2010 +0100
+++ b/src/HOLCF/Fixrec.thy	Wed Nov 03 07:02:09 2010 -0700
@@ -150,12 +150,12 @@
 definition
   match_TT :: "tr \<rightarrow> 'c match \<rightarrow> 'c match"
 where
-  "match_TT = (\<Lambda> x k. If x then k else fail fi)"
+  "match_TT = (\<Lambda> x k. If x then k else fail)"
  
 definition
   match_FF :: "tr \<rightarrow> 'c match \<rightarrow> 'c match"
 where
-  "match_FF = (\<Lambda> x k. If x then fail else k fi)"
+  "match_FF = (\<Lambda> x k. If x then fail else k)"
 
 lemma match_UU_simps [simp]:
   "match_UU\<cdot>\<bottom>\<cdot>k = \<bottom>"
@@ -222,11 +222,11 @@
 by simp
 
 lemma def_cont_fix_eq:
-  "\<lbrakk>f \<equiv> fix\<cdot>(Abs_CFun F); cont F\<rbrakk> \<Longrightarrow> f = F f"
+  "\<lbrakk>f \<equiv> fix\<cdot>(Abs_cfun F); cont F\<rbrakk> \<Longrightarrow> f = F f"
 by (simp, subst fix_eq, simp)
 
 lemma def_cont_fix_ind:
-  "\<lbrakk>f \<equiv> fix\<cdot>(Abs_CFun F); cont F; adm P; P \<bottom>; \<And>x. P x \<Longrightarrow> P (F x)\<rbrakk> \<Longrightarrow> P f"
+  "\<lbrakk>f \<equiv> fix\<cdot>(Abs_cfun F); cont F; adm P; P \<bottom>; \<And>x. P x \<Longrightarrow> P (F x)\<rbrakk> \<Longrightarrow> P f"
 by (simp add: fix_ind)
 
 text {* lemma for proving rewrite rules *}
diff -r abc52faa7761 -r 3b7f570723f9 src/HOLCF/HOLCF.thy
--- a/src/HOLCF/HOLCF.thy	Wed Nov 03 10:44:53 2010 +0100
+++ b/src/HOLCF/HOLCF.thy	Wed Nov 03 07:02:09 2010 -0700
@@ -11,7 +11,7 @@
   Powerdomains
 begin
 
-default_sort pcpo
+default_sort bifinite
 
 ML {* path_add "~~/src/HOLCF/Library" *}
 
@@ -27,6 +27,9 @@
 lemmas monofun_fun_arg = monofunE
 lemmas monofun_lub_fun = adm_monofun [THEN admD]
 lemmas cont_lub_fun = adm_cont [THEN admD]
+lemmas cont2cont_Rep_CFun = cont2cont_APP
+lemmas cont_Rep_CFun_app = cont_APP_app
+lemmas cont_Rep_CFun_app_app = cont_APP_app_app
 
 text {* Older legacy theorem names: *}
 
diff -r abc52faa7761 -r 3b7f570723f9 src/HOLCF/IOA/meta_theory/CompoExecs.thy
--- a/src/HOLCF/IOA/meta_theory/CompoExecs.thy	Wed Nov 03 10:44:53 2010 +0100
+++ b/src/HOLCF/IOA/meta_theory/CompoExecs.thy	Wed Nov 03 07:02:09 2010 -0700
@@ -39,7 +39,7 @@
     | x##xs => (flift1
             (%p.(If Def ((fst p)~:actions sig)
                  then Def (s=(snd p))
-                 else TT fi)
+                 else TT)
                 andalso (h$xs) (snd p))
              $x)
    )))"
@@ -137,7 +137,7 @@
      | x##xs => (flift1
              (%p.(If Def ((fst p)~:actions sig)
                   then Def (s=(snd p))
-                  else TT fi)
+                  else TT)
                  andalso (stutter2 sig$xs) (snd p))
               $x)
             ))"
diff -r abc52faa7761 -r 3b7f570723f9 src/HOLCF/IOA/meta_theory/Seq.thy
--- a/src/HOLCF/IOA/meta_theory/Seq.thy	Wed Nov 03 10:44:53 2010 +0100
+++ b/src/HOLCF/IOA/meta_theory/Seq.thy	Wed Nov 03 07:02:09 2010 -0700
@@ -8,7 +8,9 @@
 imports HOLCF
 begin
 
-domain 'a seq = nil  ("nil") | cons (HD :: 'a) (lazy TL :: "'a seq")  (infixr "##" 65)
+default_sort pcpo
+
+domain (unsafe) 'a seq = nil  ("nil") | cons (HD :: 'a) (lazy TL :: "'a seq")  (infixr "##" 65)
 
 (*
    sfilter       :: "('a -> tr) -> 'a seq -> 'a seq"
@@ -70,7 +72,7 @@
   sfilter_nil: "sfilter$P$nil=nil"
 | sfilter_cons:
     "x~=UU ==> sfilter$P$(x##xs)=
-              (If P$x then x##(sfilter$P$xs) else sfilter$P$xs fi)"
+              (If P$x then x##(sfilter$P$xs) else sfilter$P$xs)"
 
 lemma sfilter_UU [simp]: "sfilter$P$UU=UU"
 by fixrec_simp
@@ -98,7 +100,7 @@
   stakewhile_nil: "stakewhile$P$nil=nil"
 | stakewhile_cons:
     "x~=UU ==> stakewhile$P$(x##xs) =
-              (If P$x then x##(stakewhile$P$xs) else nil fi)"
+              (If P$x then x##(stakewhile$P$xs) else nil)"
 
 lemma stakewhile_UU [simp]: "stakewhile$P$UU=UU"
 by fixrec_simp
@@ -111,7 +113,7 @@
   sdropwhile_nil: "sdropwhile$P$nil=nil"
 | sdropwhile_cons:
     "x~=UU ==> sdropwhile$P$(x##xs) =
-              (If P$x then sdropwhile$P$xs else x##xs fi)"
+              (If P$x then sdropwhile$P$xs else x##xs)"
 
 lemma sdropwhile_UU [simp]: "sdropwhile$P$UU=UU"
 by fixrec_simp
@@ -123,7 +125,7 @@
 where
   slast_nil: "slast$nil=UU"
 | slast_cons:
-    "x~=UU ==> slast$(x##xs)= (If is_nil$xs then x else slast$xs fi)"
+    "x~=UU ==> slast$(x##xs)= (If is_nil$xs then x else slast$xs)"
 
 lemma slast_UU [simp]: "slast$UU=UU"
 by fixrec_simp
diff -r abc52faa7761 -r 3b7f570723f9 src/HOLCF/IOA/meta_theory/Sequence.thy
--- a/src/HOLCF/IOA/meta_theory/Sequence.thy	Wed Nov 03 10:44:53 2010 +0100
+++ b/src/HOLCF/IOA/meta_theory/Sequence.thy	Wed Nov 03 07:02:09 2010 -0700
@@ -901,8 +901,8 @@
 apply (rule_tac t="s1" in seq.reach [THEN subst])
 apply (rule_tac t="s2" in seq.reach [THEN subst])
 apply (rule lub_mono)
-apply (rule seq.chain_take [THEN ch2ch_Rep_CFunL])
-apply (rule seq.chain_take [THEN ch2ch_Rep_CFunL])
+apply (rule seq.chain_take [THEN ch2ch_Rep_cfunL])
+apply (rule seq.chain_take [THEN ch2ch_Rep_cfunL])
 apply (rule assms)
 done
 
diff -r abc52faa7761 -r 3b7f570723f9 src/HOLCF/Library/Stream.thy
--- a/src/HOLCF/Library/Stream.thy	Wed Nov 03 10:44:53 2010 +0100
+++ b/src/HOLCF/Library/Stream.thy	Wed Nov 03 07:02:09 2010 -0700
@@ -8,7 +8,9 @@
 imports HOLCF Nat_Infinity
 begin
 
-domain 'a stream = scons (ft::'a) (lazy rt::"'a stream") (infixr "&&" 65)
+default_sort pcpo
+
+domain (unsafe) 'a stream = scons (ft::'a) (lazy rt::"'a stream") (infixr "&&" 65)
 
 definition
   smap :: "('a \<rightarrow> 'b) \<rightarrow> 'a stream \<rightarrow> 'b stream" where
@@ -17,7 +19,7 @@
 definition
   sfilter :: "('a \<rightarrow> tr) \<rightarrow> 'a stream \<rightarrow> 'a stream" where
   "sfilter = fix\<cdot>(\<Lambda> h p s. case s of x && xs \<Rightarrow>
-                                     If p\<cdot>x then x && h\<cdot>p\<cdot>xs else h\<cdot>p\<cdot>xs fi)"
+                                     If p\<cdot>x then x && h\<cdot>p\<cdot>xs else h\<cdot>p\<cdot>xs)"
 
 definition
   slen :: "'a stream \<Rightarrow> inat"  ("#_" [1000] 1000) where
@@ -504,7 +506,7 @@
 
 lemma sfilter_unfold:
  "sfilter = (\<Lambda> p s. case s of x && xs \<Rightarrow>
-  If p\<cdot>x then x && sfilter\<cdot>p\<cdot>xs else sfilter\<cdot>p\<cdot>xs fi)"
+  If p\<cdot>x then x && sfilter\<cdot>p\<cdot>xs else sfilter\<cdot>p\<cdot>xs)"
 by (insert sfilter_def [where 'a='a, THEN eq_reflection, THEN fix_eq2], auto)
 
 lemma strict_sfilter: "sfilter\<cdot>\<bottom> = \<bottom>"
@@ -518,7 +520,7 @@
 
 lemma sfilter_scons [simp]:
   "x ~= \<bottom> ==> sfilter\<cdot>f\<cdot>(x && xs) =
-                           If f\<cdot>x then x && sfilter\<cdot>f\<cdot>xs else sfilter\<cdot>f\<cdot>xs fi"
+                           If f\<cdot>x then x && sfilter\<cdot>f\<cdot>xs else sfilter\<cdot>f\<cdot>xs"
 by (subst sfilter_unfold, force)
 
 
@@ -921,7 +923,7 @@
 by (rule monofun_cfun_arg,simp)
 
 lemma contlub_scons_lemma: "chain S ==> (LUB i. a && S i) = a && (LUB i. S i)"
-by (rule cont2contlubE [OF cont_Rep_CFun2, symmetric])
+by (rule cont2contlubE [OF cont_Rep_cfun2, symmetric])
 
 lemma finite_lub_sconc: "chain Y ==> (stream_finite x) ==>
                         (LUB i. x ooo Y i) = (x ooo (LUB i. Y i))"
diff -r abc52faa7761 -r 3b7f570723f9 src/HOLCF/Lift.thy
--- a/src/HOLCF/Lift.thy	Wed Nov 03 10:44:53 2010 +0100
+++ b/src/HOLCF/Lift.thy	Wed Nov 03 07:02:09 2010 -0700
@@ -95,6 +95,11 @@
   flift1 :: "('a \<Rightarrow> 'b::pcpo) \<Rightarrow> ('a lift \<rightarrow> 'b)"  (binder "FLIFT " 10)  where
   "flift1 = (\<lambda>f. (\<Lambda> x. lift_case \<bottom> f x))"
 
+translations
+  "\<Lambda>(XCONST Def x). t" => "CONST flift1 (\<lambda>x. t)"
+  "\<Lambda>(CONST Def x). FLIFT y. t" <= "FLIFT x y. t"
+  "\<Lambda>(CONST Def x). t" <= "FLIFT x. t"
+
 definition
   flift2 :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a lift \<rightarrow> 'b lift)" where
   "flift2 f = (FLIFT x. Def (f x))"
@@ -114,7 +119,7 @@
 lemma flift2_defined [simp]: "x \<noteq> \<bottom> \<Longrightarrow> (flift2 f)\<cdot>x \<noteq> \<bottom>"
 by (erule lift_definedE, simp)
 
-lemma flift2_defined_iff [simp]: "(flift2 f\<cdot>x = \<bottom>) = (x = \<bottom>)"
+lemma flift2_bottom_iff [simp]: "(flift2 f\<cdot>x = \<bottom>) = (x = \<bottom>)"
 by (cases x, simp_all)
 
 lemma FLIFT_mono:
diff -r abc52faa7761 -r 3b7f570723f9 src/HOLCF/LowerPD.thy
--- a/src/HOLCF/LowerPD.thy	Wed Nov 03 10:44:53 2010 +0100
+++ b/src/HOLCF/LowerPD.thy	Wed Nov 03 07:02:09 2010 -0700
@@ -229,10 +229,10 @@
 using lower_unit_Rep_compact_basis [of compact_bot]
 by (simp add: inst_lower_pd_pcpo)
 
-lemma lower_unit_strict_iff [simp]: "{x}\<flat> = \<bottom> \<longleftrightarrow> x = \<bottom>"
+lemma lower_unit_bottom_iff [simp]: "{x}\<flat> = \<bottom> \<longleftrightarrow> x = \<bottom>"
 unfolding lower_unit_strict [symmetric] by (rule lower_unit_eq_iff)
 
-lemma lower_plus_strict_iff [simp]:
+lemma lower_plus_bottom_iff [simp]:
   "xs +\<flat> ys = \<bottom> \<longleftrightarrow> xs = \<bottom> \<and> ys = \<bottom>"
 apply safe
 apply (rule UU_I, erule subst, rule lower_plus_below1)
@@ -256,7 +256,7 @@
 lemma compact_lower_unit_iff [simp]: "compact {x}\<flat> \<longleftrightarrow> compact x"
 apply (safe elim!: compact_lower_unit)
 apply (simp only: compact_def lower_unit_below_iff [symmetric])
-apply (erule adm_subst [OF cont_Rep_CFun2])
+apply (erule adm_subst [OF cont_Rep_cfun2])
 done
 
 lemma compact_lower_plus [simp]:
diff -r abc52faa7761 -r 3b7f570723f9 src/HOLCF/Pcpodef.thy
--- a/src/HOLCF/Pcpodef.thy	Wed Nov 03 10:44:53 2010 +0100
+++ b/src/HOLCF/Pcpodef.thy	Wed Nov 03 07:02:09 2010 -0700
@@ -152,13 +152,9 @@
     and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
     and adm: "adm (\<lambda>x. x \<in> A)" (* not used *)
     and f_in_A: "\<And>x. f x \<in> A"
-    and cont_f: "cont f"
-  shows "cont (\<lambda>x. Abs (f x))"
- apply (rule contI)
- apply (rule typedef_is_lubI [OF below])
- apply (simp only: type_definition.Abs_inverse [OF type f_in_A])
- apply (erule cont_f [THEN contE])
-done
+  shows "cont f \<Longrightarrow> cont (\<lambda>x. Abs (f x))"
+unfolding cont_def is_lub_def is_ub_def ball_simps below
+by (simp add: type_definition.Abs_inverse [OF type f_in_A])
 
 subsection {* Proving subtype elements are compact *}
 
@@ -235,7 +231,7 @@
  apply (rule type_definition.Abs_inverse [OF type UU_in_A])
 done
 
-theorem typedef_Abs_strict_iff:
+theorem typedef_Abs_bottom_iff:
   assumes type: "type_definition Rep Abs A"
     and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
     and UU_in_A: "\<bottom> \<in> A"
@@ -244,7 +240,7 @@
  apply (simp add: type_definition.Abs_inject [OF type] UU_in_A)
 done
 
-theorem typedef_Rep_strict_iff:
+theorem typedef_Rep_bottom_iff:
   assumes type: "type_definition Rep Abs A"
     and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
     and UU_in_A: "\<bottom> \<in> A"
@@ -258,14 +254,14 @@
     and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
     and UU_in_A: "\<bottom> \<in> A"
   shows "\<lbrakk>x \<noteq> \<bottom>; x \<in> A\<rbrakk> \<Longrightarrow> Abs x \<noteq> \<bottom>"
-by (simp add: typedef_Abs_strict_iff [OF type below UU_in_A])
+by (simp add: typedef_Abs_bottom_iff [OF type below UU_in_A])
 
 theorem typedef_Rep_defined:
   assumes type: "type_definition Rep Abs A"
     and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
     and UU_in_A: "\<bottom> \<in> A"
   shows "x \<noteq> \<bottom> \<Longrightarrow> Rep x \<noteq> \<bottom>"
-by (simp add: typedef_Rep_strict_iff [OF type below UU_in_A])
+by (simp add: typedef_Rep_bottom_iff [OF type below UU_in_A])
 
 subsection {* Proving a subtype is flat *}
 
diff -r abc52faa7761 -r 3b7f570723f9 src/HOLCF/Product_Cpo.thy
--- a/src/HOLCF/Product_Cpo.thy	Wed Nov 03 10:44:53 2010 +0100
+++ b/src/HOLCF/Product_Cpo.thy	Wed Nov 03 07:02:09 2010 -0700
@@ -173,7 +173,7 @@
 lemma inst_cprod_pcpo: "\<bottom> = (\<bottom>, \<bottom>)"
 by (rule minimal_cprod [THEN UU_I, symmetric])
 
-lemma Pair_defined_iff [simp]: "(x, y) = \<bottom> \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>"
+lemma Pair_bottom_iff [simp]: "(x, y) = \<bottom> \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>"
 unfolding inst_cprod_pcpo by simp
 
 lemma fst_strict [simp]: "fst \<bottom> = \<bottom>"
diff -r abc52faa7761 -r 3b7f570723f9 src/HOLCF/Sprod.thy
--- a/src/HOLCF/Sprod.thy	Wed Nov 03 10:44:53 2010 +0100
+++ b/src/HOLCF/Sprod.thy	Wed Nov 03 07:02:09 2010 -0700
@@ -80,7 +80,7 @@
 lemma spair_strict2 [simp]: "(:x, \<bottom>:) = \<bottom>"
 by (simp add: Rep_sprod_simps)
 
-lemma spair_strict_iff [simp]: "((:x, y:) = \<bottom>) = (x = \<bottom> \<or> y = \<bottom>)"
+lemma spair_bottom_iff [simp]: "((:x, y:) = \<bottom>) = (x = \<bottom> \<or> y = \<bottom>)"
 by (simp add: Rep_sprod_simps strict_conv_if)
 
 lemma spair_below_iff:
@@ -136,10 +136,10 @@
 lemma ssnd_spair [simp]: "x \<noteq> \<bottom> \<Longrightarrow> ssnd\<cdot>(:x, y:) = y"
 by (simp add: ssnd_def cont_Rep_sprod Rep_sprod_spair)
 
-lemma sfst_defined_iff [simp]: "(sfst\<cdot>p = \<bottom>) = (p = \<bottom>)"
+lemma sfst_bottom_iff [simp]: "(sfst\<cdot>p = \<bottom>) = (p = \<bottom>)"
 by (cases p, simp_all)
 
-lemma ssnd_defined_iff [simp]: "(ssnd\<cdot>p = \<bottom>) = (p = \<bottom>)"
+lemma ssnd_bottom_iff [simp]: "(ssnd\<cdot>p = \<bottom>) = (p = \<bottom>)"
 by (cases p, simp_all)
 
 lemma sfst_defined: "p \<noteq> \<bottom> \<Longrightarrow> sfst\<cdot>p \<noteq> \<bottom>"
diff -r abc52faa7761 -r 3b7f570723f9 src/HOLCF/Ssum.thy
--- a/src/HOLCF/Ssum.thy	Wed Nov 03 10:44:53 2010 +0100
+++ b/src/HOLCF/Ssum.thy	Wed Nov 03 07:02:09 2010 -0700
@@ -98,10 +98,10 @@
 lemma sinr_strict [simp]: "sinr\<cdot>\<bottom> = \<bottom>"
 by (simp add: Rep_ssum_simps)
 
-lemma sinl_defined_iff [simp]: "(sinl\<cdot>x = \<bottom>) = (x = \<bottom>)"
+lemma sinl_bottom_iff [simp]: "(sinl\<cdot>x = \<bottom>) = (x = \<bottom>)"
 using sinl_eq [of "x" "\<bottom>"] by simp
 
-lemma sinr_defined_iff [simp]: "(sinr\<cdot>x = \<bottom>) = (x = \<bottom>)"
+lemma sinr_bottom_iff [simp]: "(sinr\<cdot>x = \<bottom>) = (x = \<bottom>)"
 using sinr_eq [of "x" "\<bottom>"] by simp
 
 lemma sinl_defined: "x \<noteq> \<bottom> \<Longrightarrow> sinl\<cdot>x \<noteq> \<bottom>"
@@ -120,11 +120,11 @@
 
 lemma compact_sinlD: "compact (sinl\<cdot>x) \<Longrightarrow> compact x"
 unfolding compact_def
-by (drule adm_subst [OF cont_Rep_CFun2 [where f=sinl]], simp)
+by (drule adm_subst [OF cont_Rep_cfun2 [where f=sinl]], simp)
 
 lemma compact_sinrD: "compact (sinr\<cdot>x) \<Longrightarrow> compact x"
 unfolding compact_def
-by (drule adm_subst [OF cont_Rep_CFun2 [where f=sinr]], simp)
+by (drule adm_subst [OF cont_Rep_cfun2 [where f=sinr]], simp)
 
 lemma compact_sinl_iff [simp]: "compact (sinl\<cdot>x) = compact x"
 by (safe elim!: compact_sinl compact_sinlD)
@@ -160,7 +160,7 @@
 
 definition
   sscase :: "('a \<rightarrow> 'c) \<rightarrow> ('b \<rightarrow> 'c) \<rightarrow> ('a ++ 'b) \<rightarrow> 'c" where
-  "sscase = (\<Lambda> f g s. (\<lambda>(t, x, y). If t then f\<cdot>x else g\<cdot>y fi) (Rep_ssum s))"
+  "sscase = (\<Lambda> f g s. (\<lambda>(t, x, y). If t then f\<cdot>x else g\<cdot>y) (Rep_ssum s))"
 
 translations
   "case s of XCONST sinl\<cdot>x \<Rightarrow> t1 | XCONST sinr\<cdot>y \<Rightarrow> t2" == "CONST sscase\<cdot>(\<Lambda> x. t1)\<cdot>(\<Lambda> y. t2)\<cdot>s"
@@ -170,7 +170,7 @@
   "\<Lambda>(XCONST sinr\<cdot>y). t" == "CONST sscase\<cdot>\<bottom>\<cdot>(\<Lambda> y. t)"
 
 lemma beta_sscase:
-  "sscase\<cdot>f\<cdot>g\<cdot>s = (\<lambda>(t, x, y). If t then f\<cdot>x else g\<cdot>y fi) (Rep_ssum s)"
+  "sscase\<cdot>f\<cdot>g\<cdot>s = (\<lambda>(t, x, y). If t then f\<cdot>x else g\<cdot>y) (Rep_ssum s)"
 unfolding sscase_def by (simp add: cont_Rep_ssum [THEN cont_compose])
 
 lemma sscase1 [simp]: "sscase\<cdot>f\<cdot>g\<cdot>\<bottom> = \<bottom>"
diff -r abc52faa7761 -r 3b7f570723f9 src/HOLCF/Tools/Domain/domain.ML
--- a/src/HOLCF/Tools/Domain/domain.ML	Wed Nov 03 10:44:53 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain.ML	Wed Nov 03 07:02:09 2010 -0700
@@ -221,6 +221,7 @@
 (** outer syntax **)
 
 val _ = Keyword.keyword "lazy";
+val _ = Keyword.keyword "unsafe";
 
 val dest_decl : (bool * binding option * string) parser =
   Parse.$$$ "(" |-- Scan.optional (Parse.$$$ "lazy" >> K true) false --
@@ -237,11 +238,12 @@
     (Parse.$$$ "=" |-- Parse.enum1 "|" cons_decl);
 
 val domains_decl =
-  Parse.and_list1 domain_decl;
+  Scan.optional (Parse.$$$ "(" |-- (Parse.$$$ "unsafe" >> K true) --| Parse.$$$ ")") false --
+    Parse.and_list1 domain_decl;
 
 fun mk_domain
-    (definitional : bool)
-    (doms : ((((string * string option) list * binding) * mixfix) *
+    (unsafe : bool,
+     doms : ((((string * string option) list * binding) * mixfix) *
              ((binding * (bool * binding option * string) list) * mixfix) list) list ) =
   let
     val specs : ((string * string option) list * binding * mixfix *
@@ -249,17 +251,13 @@
         map (fn (((vs, t), mx), cons) =>
                 (vs, t, mx, map (fn ((c, ds), mx) => (c, ds, mx)) cons)) doms;
   in
-    if definitional
-    then add_new_domain_cmd specs
-    else add_domain_cmd specs
+    if unsafe
+    then add_domain_cmd specs
+    else add_new_domain_cmd specs
   end;
 
 val _ =
   Outer_Syntax.command "domain" "define recursive domains (HOLCF)"
-    Keyword.thy_decl (domains_decl >> (Toplevel.theory o mk_domain false));
-
-val _ =
-  Outer_Syntax.command "new_domain" "define recursive domains (HOLCF)"
-    Keyword.thy_decl (domains_decl >> (Toplevel.theory o mk_domain true));
+    Keyword.thy_decl (domains_decl >> (Toplevel.theory o mk_domain));
 
 end;
diff -r abc52faa7761 -r 3b7f570723f9 src/HOLCF/Tools/Domain/domain_constructors.ML
--- a/src/HOLCF/Tools/Domain/domain_constructors.ML	Wed Nov 03 10:44:53 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_constructors.ML	Wed Nov 03 07:02:09 2010 -0700
@@ -67,7 +67,7 @@
 val simple_ss = HOL_basic_ss addsimps simp_thms;
 
 val beta_rules =
-  @{thms beta_cfun cont_id cont_const cont2cont_Rep_CFun cont2cont_LAM'} @
+  @{thms beta_cfun cont_id cont_const cont2cont_APP cont2cont_LAM'} @
   @{thms cont2cont_fst cont2cont_snd cont2cont_Pair};
 
 val beta_ss = HOL_basic_ss addsimps (simp_thms @ beta_rules);
@@ -210,7 +210,7 @@
           in (n2, mk_ssumT (t1, t2)) end;
       val ct = ctyp_of thy (snd (cons2typ 1 spec'));
       val thm1 = instantiate' [SOME ct] [] @{thm exh_start};
-      val thm2 = rewrite_rule (map mk_meta_eq @{thms ex_defined_iffs}) thm1;
+      val thm2 = rewrite_rule (map mk_meta_eq @{thms ex_bottom_iffs}) thm1;
       val thm3 = rewrite_rule [mk_meta_eq @{thm conj_assoc}] thm2;
 
       val y = Free ("y", lhsT);
@@ -279,8 +279,8 @@
           val lhs = mk_undef (list_ccomb (con, vs));
           val rhss = map mk_undef nonlazy;
           val goal = mk_trp (iff_disj (lhs, rhss));
-          val rule1 = iso_locale RS @{thm iso.abs_defined_iff};
-          val rules = rule1 :: @{thms con_defined_iff_rules};
+          val rule1 = iso_locale RS @{thm iso.abs_bottom_iff};
+          val rules = rule1 :: @{thms con_bottom_iff_rules};
           val tacs = [simp_tac (HOL_ss addsimps rules) 1];
         in prove thy con_betas goal (K tacs) end;
     in
@@ -453,7 +453,7 @@
       fun argvars n args = map_index (argvar n) args;
       fun app s (l, r) = mk_appl (Constant s) [l, r];
       val cabs = app "_cabs";
-      val capp = app @{const_syntax Rep_CFun};
+      val capp = app @{const_syntax Rep_cfun};
       val capps = Library.foldl capp
       fun con1 authentic n (con,args) =
           Library.foldl capp (c_ast authentic con, argvars n args);
@@ -506,7 +506,7 @@
           val goal = Logic.list_implies (assms, concl);
           val defs = case_beta :: con_betas;
           val rules1 = @{thms strictify2 sscase2 sscase3 ssplit2 fup2 ID1};
-          val rules2 = @{thms con_defined_iff_rules};
+          val rules2 = @{thms con_bottom_iff_rules};
           val rules3 = @{thms cfcomp2 one_case2};
           val rules = abs_inverse :: rules1 @ rules2 @ rules3;
           val tacs = [asm_simp_tac (beta_ss addsimps rules) 1];
@@ -528,7 +528,7 @@
     (rep_const : term)
     (abs_inv : thm)
     (rep_strict : thm)
-    (rep_strict_iff : thm)
+    (rep_bottom_iff : thm)
     (con_betas : thm list)
     (thy : theory)
     : thm list * theory =
@@ -637,7 +637,7 @@
   (* prove selector definedness rules *)
     val sel_defins : thm list =
       let
-        val rules = rep_strict_iff :: @{thms sel_defined_iff_rules};
+        val rules = rep_bottom_iff :: @{thms sel_bottom_iff_rules};
         val tacs = [simp_tac (HOL_basic_ss addsimps rules) 1];
         fun sel_defin sel =
           let
@@ -868,8 +868,8 @@
     val iso_locale = @{thm iso.intro} OF [abs_iso_thm, rep_iso_thm];
     val rep_strict = iso_locale RS @{thm iso.rep_strict};
     val abs_strict = iso_locale RS @{thm iso.abs_strict};
-    val rep_defined_iff = iso_locale RS @{thm iso.rep_defined_iff};
-    val abs_defined_iff = iso_locale RS @{thm iso.abs_defined_iff};
+    val rep_bottom_iff = iso_locale RS @{thm iso.rep_bottom_iff};
+    val abs_bottom_iff = iso_locale RS @{thm iso.abs_bottom_iff};
     val iso_rews = [abs_iso_thm, rep_iso_thm, abs_strict, rep_strict];
 
     (* qualify constants and theorems with domain name *)
@@ -908,7 +908,7 @@
           map2 (fn con => fn (b, args, mx) => (con, args)) con_consts spec;
       in
         add_selectors sel_spec rep_const
-          abs_iso_thm rep_strict rep_defined_iff con_betas thy
+          abs_iso_thm rep_strict rep_bottom_iff con_betas thy
       end;
 
     (* define and prove theorems for discriminator functions *)
diff -r abc52faa7761 -r 3b7f570723f9 src/HOLCF/Tools/Domain/domain_induction.ML
--- a/src/HOLCF/Tools/Domain/domain_induction.ML	Wed Nov 03 10:44:53 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_induction.ML	Wed Nov 03 07:02:09 2010 -0700
@@ -132,7 +132,7 @@
       mk_trp (p $ HOLCF_Library.mk_bottom T) :: map (con_assm true p) cons;
   val assms = maps eq_assms (Ps ~~ newTs ~~ map #con_specs constr_infos);
 
-  val take_ss = HOL_ss addsimps (@{thm Rep_CFun_strict1} :: take_rews);
+  val take_ss = HOL_ss addsimps (@{thm Rep_cfun_strict1} :: take_rews);
   fun quant_tac ctxt i = EVERY
     (map (fn name => res_inst_tac ctxt [(("x", 0), name)] spec i) x_names);
 
@@ -317,7 +317,7 @@
         end;
       val goal =
           mk_trp (foldr1 mk_conj (map one (newTs ~~ Rs ~~ take_consts)));
-      val rules = @{thm Rep_CFun_strict1} :: take_0_thms;
+      val rules = @{thm Rep_cfun_strict1} :: take_0_thms;
       fun tacf {prems, context} =
         let
           val prem' = rewrite_rule [bisim_def_thm] (hd prems);
diff -r abc52faa7761 -r 3b7f570723f9 src/HOLCF/Tools/Domain/domain_isomorphism.ML
--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Wed Nov 03 10:44:53 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Wed Nov 03 07:02:09 2010 -0700
@@ -38,7 +38,7 @@
 struct
 
 val beta_rules =
-  @{thms beta_cfun cont_id cont_const cont2cont_Rep_CFun cont2cont_LAM'} @
+  @{thms beta_cfun cont_id cont_const cont2cont_APP cont2cont_LAM'} @
   @{thms cont2cont_fst cont2cont_snd cont2cont_Pair cont2cont_prod_case'};
 
 val beta_ss = HOL_basic_ss addsimps (simp_thms @ beta_rules);
@@ -155,7 +155,7 @@
     (* convert parameters to lambda abstractions *)
     fun mk_eqn (lhs, rhs) =
         case lhs of
-          Const (@{const_name Rep_CFun}, _) $ f $ (x as Free _) =>
+          Const (@{const_name Rep_cfun}, _) $ f $ (x as Free _) =>
             mk_eqn (f, big_lambda x rhs)
         | f $ Const (@{const_name TYPE}, T) =>
             mk_eqn (f, Abs ("t", T, rhs))
diff -r abc52faa7761 -r 3b7f570723f9 src/HOLCF/Tools/Domain/domain_take_proofs.ML
--- a/src/HOLCF/Tools/Domain/domain_take_proofs.ML	Wed Nov 03 10:44:53 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_take_proofs.ML	Wed Nov 03 07:02:09 2010 -0700
@@ -106,7 +106,7 @@
   };
 
 val beta_rules =
-  @{thms beta_cfun cont_id cont_const cont2cont_Rep_CFun cont2cont_LAM'} @
+  @{thms beta_cfun cont_id cont_const cont2cont_APP cont2cont_LAM'} @
   @{thms cont2cont_fst cont2cont_snd cont2cont_Pair};
 
 val beta_ss = HOL_basic_ss addsimps (simp_thms @ beta_rules);
diff -r abc52faa7761 -r 3b7f570723f9 src/HOLCF/Tools/cont_consts.ML
--- a/src/HOLCF/Tools/cont_consts.ML	Wed Nov 03 10:44:53 2010 +0100
+++ b/src/HOLCF/Tools/cont_consts.ML	Wed Nov 03 07:02:09 2010 -0700
@@ -28,7 +28,7 @@
   in
     [Syntax.ParsePrintRule
       (Syntax.mk_appl (Constant name2) (map Variable vnames),
-        fold (fn a => fn t => Syntax.mk_appl (Constant @{const_syntax Rep_CFun}) [t, Variable a])
+        fold (fn a => fn t => Syntax.mk_appl (Constant @{const_syntax Rep_cfun}) [t, Variable a])
           vnames (Constant name1))] @
     (case mx of
       Infix _ => [extra_parse_rule]
diff -r abc52faa7761 -r 3b7f570723f9 src/HOLCF/Tools/cont_proc.ML
--- a/src/HOLCF/Tools/cont_proc.ML	Wed Nov 03 10:44:53 2010 +0100
+++ b/src/HOLCF/Tools/cont_proc.ML	Wed Nov 03 07:02:09 2010 -0700
@@ -19,19 +19,19 @@
 
 val cont_K = @{thm cont_const};
 val cont_I = @{thm cont_id};
-val cont_A = @{thm cont2cont_Rep_CFun};
+val cont_A = @{thm cont2cont_APP};
 val cont_L = @{thm cont2cont_LAM};
-val cont_R = @{thm cont_Rep_CFun2};
+val cont_R = @{thm cont_Rep_cfun2};
 
 (* checks whether a term contains no dangling bound variables *)
 fun is_closed_term t = not (Term.loose_bvar (t, 0));
 
 (* checks whether a term is written entirely in the LCF sublanguage *)
-fun is_lcf_term (Const (@{const_name Rep_CFun}, _) $ t $ u) =
+fun is_lcf_term (Const (@{const_name Rep_cfun}, _) $ t $ u) =
       is_lcf_term t andalso is_lcf_term u
-  | is_lcf_term (Const (@{const_name Abs_CFun}, _) $ Abs (_, _, t)) =
+  | is_lcf_term (Const (@{const_name Abs_cfun}, _) $ Abs (_, _, t)) =
       is_lcf_term t
-  | is_lcf_term (Const (@{const_name Abs_CFun}, _) $ t) =
+  | is_lcf_term (Const (@{const_name Abs_cfun}, _) $ t) =
       is_lcf_term (Term.incr_boundvars 1 t $ Bound 0)
   | is_lcf_term (Bound _) = true
   | is_lcf_term t = is_closed_term t;
@@ -67,17 +67,17 @@
   (* first list: cont thm for each dangling bound variable *)
   (* second list: cont thm for each LAM in t *)
   (* if b = false, only return cont thm for outermost LAMs *)
-  fun cont_thms1 b (Const (@{const_name Rep_CFun}, _) $ f $ t) =
+  fun cont_thms1 b (Const (@{const_name Rep_cfun}, _) $ f $ t) =
     let
       val (cs1,ls1) = cont_thms1 b f;
       val (cs2,ls2) = cont_thms1 b t;
     in (zip cs1 cs2, if b then ls1 @ ls2 else []) end
-    | cont_thms1 b (Const (@{const_name Abs_CFun}, _) $ Abs (_, _, t)) =
+    | cont_thms1 b (Const (@{const_name Abs_cfun}, _) $ Abs (_, _, t)) =
     let
       val (cs, ls) = cont_thms1 b t;
       val (cs', l) = lam cs;
     in (cs', l::ls) end
-    | cont_thms1 b (Const (@{const_name Abs_CFun}, _) $ t) =
+    | cont_thms1 b (Const (@{const_name Abs_cfun}, _) $ t) =
     let
       val t' = Term.incr_boundvars 1 t $ Bound 0;
       val (cs, ls) = cont_thms1 b t';
@@ -109,7 +109,7 @@
 
     fun cont_tac_of_term (Const (@{const_name cont}, _) $ f) =
       let
-        val f' = Const (@{const_name Abs_CFun}, dummyT) $ f;
+        val f' = Const (@{const_name Abs_cfun}, dummyT) $ f;
       in
         if is_lcf_term f'
         then new_cont_tac f'
diff -r abc52faa7761 -r 3b7f570723f9 src/HOLCF/Tools/fixrec.ML
--- a/src/HOLCF/Tools/fixrec.ML	Wed Nov 03 10:44:53 2010 +0100
+++ b/src/HOLCF/Tools/fixrec.ML	Wed Nov 03 07:02:09 2010 -0700
@@ -65,7 +65,7 @@
 fun dest_eqs t = HOLogic.dest_eq (HOLogic.dest_Trueprop t);
 
 (* similar to Thm.head_of, but for continuous application *)
-fun chead_of (Const(@{const_name Rep_CFun},_)$f$t) = chead_of f
+fun chead_of (Const(@{const_name Rep_cfun},_)$f$t) = chead_of f
   | chead_of u = u;
 
 infix 0 ==;  val (op ==) = Logic.mk_equals;
@@ -82,7 +82,7 @@
     val run = Const(@{const_name Fixrec.run}, mT ->> T)
   in
     case t of
-      Const(@{const_name Rep_CFun}, _) $
+      Const(@{const_name Rep_cfun}, _) $
         Const(@{const_name Fixrec.succeed}, _) $ u => u
     | _ => run ` t
   end;
@@ -226,7 +226,7 @@
     (* compiles a monadic term for a constructor pattern *)
     and comp_con T p rhs vs taken =
       case p of
-        Const(@{const_name Rep_CFun},_) $ f $ x =>
+        Const(@{const_name Rep_cfun},_) $ f $ x =>
           let val (rhs', v, taken') = comp_pat x rhs taken
           in comp_con T f rhs' (v::vs) taken' end
       | f $ x =>
@@ -250,7 +250,7 @@
 (* returns (constant, (vars, matcher)) *)
 fun compile_lhs match_name pat rhs vs taken =
   case pat of
-    Const(@{const_name Rep_CFun}, _) $ f $ x =>
+    Const(@{const_name Rep_cfun}, _) $ f $ x =>
       let val (rhs', v, taken') = compile_pat match_name x rhs taken;
       in compile_lhs match_name f rhs' (v::vs) taken' end
   | Free(_,_) => (pat, (vs, rhs))
diff -r abc52faa7761 -r 3b7f570723f9 src/HOLCF/Tools/holcf_library.ML
--- a/src/HOLCF/Tools/holcf_library.ML	Wed Nov 03 10:44:53 2010 +0100
+++ b/src/HOLCF/Tools/holcf_library.ML	Wed Nov 03 07:02:09 2010 -0700
@@ -76,10 +76,10 @@
   | dest_cfunT T = raise TYPE ("dest_cfunT", [T], []);
 
 fun capply_const (S, T) =
-  Const(@{const_name Rep_CFun}, (S ->> T) --> (S --> T));
+  Const(@{const_name Rep_cfun}, (S ->> T) --> (S --> T));
 
 fun cabs_const (S, T) =
-  Const(@{const_name Abs_CFun}, (S --> T) --> (S ->> T));
+  Const(@{const_name Abs_cfun}, (S --> T) --> (S ->> T));
 
 fun mk_cabs t =
   let val T = fastype_of t
diff -r abc52faa7761 -r 3b7f570723f9 src/HOLCF/Tools/pcpodef.ML
--- a/src/HOLCF/Tools/pcpodef.ML	Wed Nov 03 10:44:53 2010 +0100
+++ b/src/HOLCF/Tools/pcpodef.ML	Wed Nov 03 07:02:09 2010 -0700
@@ -11,7 +11,7 @@
     { below_def: thm, adm: thm, cont_Rep: thm, cont_Abs: thm,
       lub: thm, thelub: thm, compact: thm }
   type pcpo_info =
-    { Rep_strict: thm, Abs_strict: thm, Rep_strict_iff: thm, Abs_strict_iff: thm,
+    { Rep_strict: thm, Abs_strict: thm, Rep_bottom_iff: thm, Abs_bottom_iff: thm,
       Rep_defined: thm, Abs_defined: thm }
 
   val add_podef: bool -> binding option -> binding * (string * sort) list * mixfix ->
@@ -48,7 +48,7 @@
     lub: thm, thelub: thm, compact: thm }
 
 type pcpo_info =
-  { Rep_strict: thm, Abs_strict: thm, Rep_strict_iff: thm, Abs_strict_iff: thm,
+  { Rep_strict: thm, Abs_strict: thm, Rep_bottom_iff: thm, Abs_bottom_iff: thm,
     Rep_defined: thm, Abs_defined: thm }
 
 (* building terms *)
@@ -136,8 +136,8 @@
     fun make thm = Drule.zero_var_indexes (thm OF pcpo_thms');
     val Rep_strict = make @{thm typedef_Rep_strict};
     val Abs_strict = make @{thm typedef_Abs_strict};
-    val Rep_strict_iff = make @{thm typedef_Rep_strict_iff};
-    val Abs_strict_iff = make @{thm typedef_Abs_strict_iff};
+    val Rep_bottom_iff = make @{thm typedef_Rep_bottom_iff};
+    val Abs_bottom_iff = make @{thm typedef_Abs_bottom_iff};
     val Rep_defined = make @{thm typedef_Rep_defined};
     val Abs_defined = make @{thm typedef_Abs_defined};
     val (_, thy) =
@@ -146,14 +146,14 @@
       |> Global_Theory.add_thms
         ([((Binding.suffix_name "_strict"     Rep_name, Rep_strict), []),
           ((Binding.suffix_name "_strict"     Abs_name, Abs_strict), []),
-          ((Binding.suffix_name "_strict_iff" Rep_name, Rep_strict_iff), []),
-          ((Binding.suffix_name "_strict_iff" Abs_name, Abs_strict_iff), []),
+          ((Binding.suffix_name "_bottom_iff" Rep_name, Rep_bottom_iff), []),
+          ((Binding.suffix_name "_bottom_iff" Abs_name, Abs_bottom_iff), []),
           ((Binding.suffix_name "_defined"    Rep_name, Rep_defined), []),
           ((Binding.suffix_name "_defined"    Abs_name, Abs_defined), [])])
       ||> Sign.parent_path;
     val pcpo_info =
       { Rep_strict = Rep_strict, Abs_strict = Abs_strict,
-        Rep_strict_iff = Rep_strict_iff, Abs_strict_iff = Abs_strict_iff,
+        Rep_bottom_iff = Rep_bottom_iff, Abs_bottom_iff = Abs_bottom_iff,
         Rep_defined = Rep_defined, Abs_defined = Abs_defined };
   in
     (pcpo_info, thy)
diff -r abc52faa7761 -r 3b7f570723f9 src/HOLCF/Tr.thy
--- a/src/HOLCF/Tr.thy	Wed Nov 03 10:44:53 2010 +0100
+++ b/src/HOLCF/Tr.thy	Wed Nov 03 07:02:09 2010 -0700
@@ -64,36 +64,37 @@
 
 default_sort pcpo
 
-definition
-  trifte :: "'c \<rightarrow> 'c \<rightarrow> tr \<rightarrow> 'c" where
-  ifte_def: "trifte = (\<Lambda> t e. FLIFT b. if b then t else e)"
+definition tr_case :: "'a \<rightarrow> 'a \<rightarrow> tr \<rightarrow> 'a" where
+  "tr_case = (\<Lambda> t e (Def b). if b then t else e)"
+
 abbreviation
-  cifte_syn :: "[tr, 'c, 'c] \<Rightarrow> 'c"  ("(3If _/ (then _/ else _) fi)" 60)  where
-  "If b then e1 else e2 fi == trifte\<cdot>e1\<cdot>e2\<cdot>b"
+  cifte_syn :: "[tr, 'c, 'c] \<Rightarrow> 'c"  ("(If (_)/ then (_)/ else (_))" [0, 0, 60] 60)
+where
+  "If b then e1 else e2 == tr_case\<cdot>e1\<cdot>e2\<cdot>b"
 
 translations
-  "\<Lambda> (XCONST TT). t" == "CONST trifte\<cdot>t\<cdot>\<bottom>"
-  "\<Lambda> (XCONST FF). t" == "CONST trifte\<cdot>\<bottom>\<cdot>t"
+  "\<Lambda> (XCONST TT). t" == "CONST tr_case\<cdot>t\<cdot>\<bottom>"
+  "\<Lambda> (XCONST FF). t" == "CONST tr_case\<cdot>\<bottom>\<cdot>t"
 
 lemma ifte_thms [simp]:
-  "If \<bottom> then e1 else e2 fi = \<bottom>"
-  "If FF then e1 else e2 fi = e2"
-  "If TT then e1 else e2 fi = e1"
-by (simp_all add: ifte_def TT_def FF_def)
+  "If \<bottom> then e1 else e2 = \<bottom>"
+  "If FF then e1 else e2 = e2"
+  "If TT then e1 else e2 = e1"
+by (simp_all add: tr_case_def TT_def FF_def)
 
 
 subsection {* Boolean connectives *}
 
 definition
   trand :: "tr \<rightarrow> tr \<rightarrow> tr" where
-  andalso_def: "trand = (\<Lambda> x y. If x then y else FF fi)"
+  andalso_def: "trand = (\<Lambda> x y. If x then y else FF)"
 abbreviation
   andalso_syn :: "tr \<Rightarrow> tr \<Rightarrow> tr"  ("_ andalso _" [36,35] 35)  where
   "x andalso y == trand\<cdot>x\<cdot>y"
 
 definition
   tror :: "tr \<rightarrow> tr \<rightarrow> tr" where
-  orelse_def: "tror = (\<Lambda> x y. If x then TT else y fi)"
+  orelse_def: "tror = (\<Lambda> x y. If x then TT else y)"
 abbreviation
   orelse_syn :: "tr \<Rightarrow> tr \<Rightarrow> tr"  ("_ orelse _"  [31,30] 30)  where
   "x orelse y == tror\<cdot>x\<cdot>y"
@@ -104,11 +105,11 @@
 
 definition
   If2 :: "[tr, 'c, 'c] \<Rightarrow> 'c" where
-  "If2 Q x y = (If Q then x else y fi)"
+  "If2 Q x y = (If Q then x else y)"
 
 text {* tactic for tr-thms with case split *}
 
-lemmas tr_defs = andalso_def orelse_def neg_def ifte_def TT_def FF_def
+lemmas tr_defs = andalso_def orelse_def neg_def tr_case_def TT_def FF_def
 
 text {* lemmas about andalso, orelse, neg and if *}
 
@@ -182,7 +183,7 @@
 by (simp add: TT_def)
 
 lemma If_and_if:
-  "(If Def P then A else B fi) = (if P then A else B)"
+  "(If Def P then A else B) = (if P then A else B)"
 apply (rule_tac p = "Def P" in trE)
 apply (auto simp add: TT_def[symmetric] FF_def[symmetric])
 done
diff -r abc52faa7761 -r 3b7f570723f9 src/HOLCF/Tutorial/Domain_ex.thy
--- a/src/HOLCF/Tutorial/Domain_ex.thy	Wed Nov 03 10:44:53 2010 +0100
+++ b/src/HOLCF/Tutorial/Domain_ex.thy	Wed Nov 03 07:02:09 2010 -0700
@@ -105,19 +105,21 @@
 
 text {* Lazy constructor arguments may have unpointed types. *}
 
-domain natlist = nnil | ncons (lazy "nat discr") natlist
+domain (unsafe) natlist = nnil | ncons (lazy "nat discr") natlist
 
 text {* Class constraints may be given for type parameters on the LHS. *}
 
-domain ('a::cpo) box = Box (lazy 'a)
+domain (unsafe) ('a::cpo) box = Box (lazy 'a)
+
+domain (unsafe) ('a::type) stream = snil | scons (lazy "'a discr") "'a stream"
 
 
 subsection {* Generated constants and theorems *}
 
 domain 'a tree = Leaf (lazy 'a) | Node (left :: "'a tree") (right :: "'a tree")
 
-lemmas tree_abs_defined_iff =
-  iso.abs_defined_iff [OF iso.intro [OF tree.abs_iso tree.rep_iso]]
+lemmas tree_abs_bottom_iff =
+  iso.abs_bottom_iff [OF iso.intro [OF tree.abs_iso tree.rep_iso]]
 
 text {* Rules about ismorphism *}
 term tree_rep
@@ -196,11 +198,4 @@
   -- "Inner syntax error: unexpected end of input"
 *)
 
-text {*
-  Non-cpo type parameters currently do not work.
-*}
-(*
-domain ('a::type) stream = snil | scons (lazy "'a discr") "'a stream"
-*)
-
 end
diff -r abc52faa7761 -r 3b7f570723f9 src/HOLCF/Tutorial/New_Domain.thy
--- a/src/HOLCF/Tutorial/New_Domain.thy	Wed Nov 03 10:44:53 2010 +0100
+++ b/src/HOLCF/Tutorial/New_Domain.thy	Wed Nov 03 07:02:09 2010 -0700
@@ -9,8 +9,8 @@
 begin
 
 text {*
-  The definitional domain package only works with bifinite domains,
-  i.e. types in class @{text bifinite}.
+  UPDATE: The definitional back-end is now the default mode of the domain
+  package. This file should be merged with @{text Domain_ex.thy}.
 *}
 
 default_sort bifinite
@@ -21,7 +21,7 @@
   domain package.
 *}
 
-new_domain 'a llist = LNil | LCons (lazy 'a) (lazy "'a llist")
+domain 'a llist = LNil | LCons (lazy 'a) (lazy "'a llist")
 
 text {*
   The difference is that the new domain package is completely
@@ -38,7 +38,7 @@
   indirect recursion through the lazy list type constructor.
 *}
 
-new_domain 'a ltree = Leaf (lazy 'a) | Branch (lazy "'a ltree llist")
+domain 'a ltree = Leaf (lazy 'a) | Branch (lazy "'a ltree llist")
 
 text {*
   For indirect-recursive definitions, the domain package is not able to
diff -r abc52faa7761 -r 3b7f570723f9 src/HOLCF/Up.thy
--- a/src/HOLCF/Up.thy	Wed Nov 03 10:44:53 2010 +0100
+++ b/src/HOLCF/Up.thy	Wed Nov 03 07:02:09 2010 -0700
@@ -237,7 +237,7 @@
 
 lemma compact_upD: "compact (up\<cdot>x) \<Longrightarrow> compact x"
 unfolding compact_def
-by (drule adm_subst [OF cont_Rep_CFun2 [where f=up]], simp)
+by (drule adm_subst [OF cont_Rep_cfun2 [where f=up]], simp)
 
 lemma compact_up_iff [simp]: "compact (up\<cdot>x) = compact x"
 by (safe elim!: compact_up compact_upD)
diff -r abc52faa7761 -r 3b7f570723f9 src/HOLCF/UpperPD.thy
--- a/src/HOLCF/UpperPD.thy	Wed Nov 03 10:44:53 2010 +0100
+++ b/src/HOLCF/UpperPD.thy	Wed Nov 03 07:02:09 2010 -0700
@@ -233,10 +233,10 @@
 lemma upper_plus_strict2 [simp]: "xs +\<sharp> \<bottom> = \<bottom>"
 by (rule UU_I, rule upper_plus_below2)
 
-lemma upper_unit_strict_iff [simp]: "{x}\<sharp> = \<bottom> \<longleftrightarrow> x = \<bottom>"
+lemma upper_unit_bottom_iff [simp]: "{x}\<sharp> = \<bottom> \<longleftrightarrow> x = \<bottom>"
 unfolding upper_unit_strict [symmetric] by (rule upper_unit_eq_iff)
 
-lemma upper_plus_strict_iff [simp]:
+lemma upper_plus_bottom_iff [simp]:
   "xs +\<sharp> ys = \<bottom> \<longleftrightarrow> xs = \<bottom> \<or> ys = \<bottom>"
 apply (rule iffI)
 apply (erule rev_mp)
@@ -252,7 +252,7 @@
 lemma compact_upper_unit_iff [simp]: "compact {x}\<sharp> \<longleftrightarrow> compact x"
 apply (safe elim!: compact_upper_unit)
 apply (simp only: compact_def upper_unit_below_iff [symmetric])
-apply (erule adm_subst [OF cont_Rep_CFun2])
+apply (erule adm_subst [OF cont_Rep_cfun2])
 done
 
 lemma compact_upper_plus [simp]:
diff -r abc52faa7761 -r 3b7f570723f9 src/HOLCF/ex/Domain_Proofs.thy
--- a/src/HOLCF/ex/Domain_Proofs.thy	Wed Nov 03 10:44:53 2010 +0100
+++ b/src/HOLCF/ex/Domain_Proofs.thy	Wed Nov 03 07:02:09 2010 -0700
@@ -31,7 +31,7 @@
   foo_bar_baz_deflF ::
     "defl \<rightarrow> defl \<times> defl \<times> defl \<rightarrow> defl \<times> defl \<times> defl"
 where
-  "foo_bar_baz_deflF = (\<Lambda> a. Abs_CFun (\<lambda>(t1, t2, t3). 
+  "foo_bar_baz_deflF = (\<Lambda> a. Abs_cfun (\<lambda>(t1, t2, t3). 
     ( ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>(u_defl\<cdot>a)\<cdot>(u_defl\<cdot>t2))
     , u_defl\<cdot>(cfun_defl\<cdot>t3\<cdot>DEFL(tr))
     , u_defl\<cdot>(cfun_defl\<cdot>(convex_defl\<cdot>t1)\<cdot>DEFL(tr)))))"
@@ -269,7 +269,7 @@
      ('a foo \<rightarrow> 'b foo) \<times> ('a bar \<rightarrow> 'b bar) \<times> ('b baz \<rightarrow> 'a baz) \<rightarrow>
      ('a foo \<rightarrow> 'b foo) \<times> ('a bar \<rightarrow> 'b bar) \<times> ('b baz \<rightarrow> 'a baz)"
 where
-  "foo_bar_baz_mapF = (\<Lambda> f. Abs_CFun (\<lambda>(d1, d2, d3).
+  "foo_bar_baz_mapF = (\<Lambda> f. Abs_cfun (\<lambda>(d1, d2, d3).
     (
       foo_abs oo
         ssum_map\<cdot>ID\<cdot>(sprod_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>d2))
diff -r abc52faa7761 -r 3b7f570723f9 src/HOLCF/ex/Hoare.thy
--- a/src/HOLCF/ex/Hoare.thy	Wed Nov 03 10:44:53 2010 +0100
+++ b/src/HOLCF/ex/Hoare.thy	Wed Nov 03 07:02:09 2010 -0700
@@ -30,11 +30,11 @@
 
 definition
   p :: "'a -> 'a" where
-  "p = fix$(LAM f. LAM x. If b1$x then f$(g$x) else x fi)"
+  "p = fix$(LAM f. LAM x. If b1$x then f$(g$x) else x)"
 
 definition
   q :: "'a -> 'a" where
-  "q = fix$(LAM f. LAM x. If b1$x orelse b2$x then f$(g$x) else x fi)"
+  "q = fix$(LAM f. LAM x. If b1$x orelse b2$x then f$(g$x) else x)"
 
 
 (* --------- pure HOLCF logic, some little lemmas ------ *)
@@ -102,13 +102,13 @@
 
 (* ----- access to definitions ----- *)
 
-lemma p_def3: "p$x = If b1$x then p$(g$x) else x fi"
+lemma p_def3: "p$x = If b1$x then p$(g$x) else x"
 apply (rule trans)
 apply (rule p_def [THEN eq_reflection, THEN fix_eq3])
 apply simp
 done
 
-lemma q_def3: "q$x = If b1$x orelse b2$x then q$(g$x) else x fi"
+lemma q_def3: "q$x = If b1$x orelse b2$x then q$(g$x) else x"
 apply (rule trans)
 apply (rule q_def [THEN eq_reflection, THEN fix_eq3])
 apply simp
diff -r abc52faa7761 -r 3b7f570723f9 src/HOLCF/ex/Loop.thy
--- a/src/HOLCF/ex/Loop.thy	Wed Nov 03 10:44:53 2010 +0100
+++ b/src/HOLCF/ex/Loop.thy	Wed Nov 03 07:02:09 2010 -0700
@@ -10,23 +10,23 @@
 
 definition
   step  :: "('a -> tr)->('a -> 'a)->'a->'a" where
-  "step = (LAM b g x. If b$x then g$x else x fi)"
+  "step = (LAM b g x. If b$x then g$x else x)"
 
 definition
   while :: "('a -> tr)->('a -> 'a)->'a->'a" where
-  "while = (LAM b g. fix$(LAM f x. If b$x then f$(g$x) else x fi))"
+  "while = (LAM b g. fix$(LAM f x. If b$x then f$(g$x) else x))"
 
 (* ------------------------------------------------------------------------- *)
 (* access to definitions                                                     *)
 (* ------------------------------------------------------------------------- *)
 
 
-lemma step_def2: "step$b$g$x = If b$x then g$x else x fi"
+lemma step_def2: "step$b$g$x = If b$x then g$x else x"
 apply (unfold step_def)
 apply simp
 done
 
-lemma while_def2: "while$b$g = fix$(LAM f x. If b$x then f$(g$x) else x fi)"
+lemma while_def2: "while$b$g = fix$(LAM f x. If b$x then f$(g$x) else x)"
 apply (unfold while_def)
 apply simp
 done
@@ -36,7 +36,7 @@
 (* rekursive properties of while                                             *)
 (* ------------------------------------------------------------------------- *)
 
-lemma while_unfold: "while$b$g$x = If b$x then while$b$g$(g$x) else x fi"
+lemma while_unfold: "while$b$g$x = If b$x then while$b$g$(g$x) else x"
 apply (rule trans)
 apply (rule while_def2 [THEN fix_eq5])
 apply simp
diff -r abc52faa7761 -r 3b7f570723f9 src/HOLCF/ex/Pattern_Match.thy
--- a/src/HOLCF/ex/Pattern_Match.thy	Wed Nov 03 10:44:53 2010 +0100
+++ b/src/HOLCF/ex/Pattern_Match.thy	Wed Nov 03 07:02:09 2010 -0700
@@ -8,6 +8,8 @@
 imports HOLCF
 begin
 
+default_sort pcpo
+
 text {* FIXME: Find a proper way to un-hide constants. *}
 
 abbreviation fail :: "'a match"
@@ -115,9 +117,9 @@
 
 parse_translation {*
 (* rewrite (_pat x) => (succeed) *)
-(* rewrite (_variable x t) => (Abs_CFun (%x. t)) *)
+(* rewrite (_variable x t) => (Abs_cfun (%x. t)) *)
  [(@{syntax_const "_pat"}, fn _ => Syntax.const @{const_syntax Fixrec.succeed}),
-  mk_binder_tr (@{syntax_const "_variable"}, @{const_syntax Abs_CFun})];
+  mk_binder_tr (@{syntax_const "_variable"}, @{const_syntax Abs_cfun})];
 *}
 
 text {* Printing Case expressions *}
@@ -127,14 +129,14 @@
 
 print_translation {*
   let
-    fun dest_LAM (Const (@{const_syntax Rep_CFun},_) $ Const (@{const_syntax unit_when},_) $ t) =
+    fun dest_LAM (Const (@{const_syntax Rep_cfun},_) $ Const (@{const_syntax unit_when},_) $ t) =
           (Syntax.const @{syntax_const "_noargs"}, t)
-    |   dest_LAM (Const (@{const_syntax Rep_CFun},_) $ Const (@{const_syntax csplit},_) $ t) =
+    |   dest_LAM (Const (@{const_syntax Rep_cfun},_) $ Const (@{const_syntax csplit},_) $ t) =
           let
             val (v1, t1) = dest_LAM t;
             val (v2, t2) = dest_LAM t1;
           in (Syntax.const @{syntax_const "_args"} $ v1 $ v2, t2) end
-    |   dest_LAM (Const (@{const_syntax Abs_CFun},_) $ t) =
+    |   dest_LAM (Const (@{const_syntax Abs_cfun},_) $ t) =
           let
             val abs =
               case t of Abs abs => abs
@@ -149,7 +151,7 @@
               (Syntax.const @{syntax_const "_match"} $ p $ v) $ t
           end;
 
-  in [(@{const_syntax Rep_CFun}, Case1_tr')] end;
+  in [(@{const_syntax Rep_cfun}, Case1_tr')] end;
 *}
 
 translations
@@ -184,11 +186,11 @@
 
 definition
   TT_pat :: "(tr, unit) pat" where
-  "TT_pat = (\<Lambda> b. If b then succeed\<cdot>() else fail fi)"
+  "TT_pat = (\<Lambda> b. If b then succeed\<cdot>() else fail)"
 
 definition
   FF_pat :: "(tr, unit) pat" where
-  "FF_pat = (\<Lambda> b. If b then fail else succeed\<cdot>() fi)"
+  "FF_pat = (\<Lambda> b. If b then fail else succeed\<cdot>())"
 
 definition
   ONE_pat :: "(one, unit) pat" where
@@ -363,7 +365,7 @@
 infix 9 ` ;
 
 val beta_rules =
-  @{thms beta_cfun cont_id cont_const cont2cont_Rep_CFun cont2cont_LAM'} @
+  @{thms beta_cfun cont_id cont_const cont2cont_APP cont2cont_LAM'} @
   @{thms cont2cont_fst cont2cont_snd cont2cont_Pair};
 
 val beta_ss = HOL_basic_ss addsimps (simp_thms @ beta_rules);
@@ -485,7 +487,7 @@
       open Syntax
       fun syntax c = Syntax.mark_const (fst (dest_Const c));
       fun app s (l, r) = Syntax.mk_appl (Constant s) [l, r];
-      val capp = app @{const_syntax Rep_CFun};
+      val capp = app @{const_syntax Rep_cfun};
       val capps = Library.foldl capp
 
       fun app_var x = Syntax.mk_appl (Constant "_variable") [x, Variable "rhs"];