# HG changeset patch
# User huffman
# Date 1288212858 25200
# Node ID d065b195ec8962de6ca875196f1624702ba8a61a
# Parent  b283680d8044a78c65e5badf1169f6996330e2c6
rename lemmas *_defined_iff and *_strict_iff to *_bottom_iff

diff -r b283680d8044 -r d065b195ec89 src/HOLCF/ConvexPD.thy
--- a/src/HOLCF/ConvexPD.thy	Wed Oct 27 11:11:35 2010 -0700
+++ b/src/HOLCF/ConvexPD.thy	Wed Oct 27 13:54:18 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>"
diff -r b283680d8044 -r d065b195ec89 src/HOLCF/Deflation.thy
--- a/src/HOLCF/Deflation.thy	Wed Oct 27 11:11:35 2010 -0700
+++ b/src/HOLCF/Deflation.thy	Wed Oct 27 13:54:18 2010 -0700
@@ -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 b283680d8044 -r d065b195ec89 src/HOLCF/Domain.thy
--- a/src/HOLCF/Domain.thy	Wed Oct 27 11:11:35 2010 -0700
+++ b/src/HOLCF/Domain.thy	Wed Oct 27 13:54:18 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 b283680d8044 -r d065b195ec89 src/HOLCF/Domain_Aux.thy
--- a/src/HOLCF/Domain_Aux.thy	Wed Oct 27 11:11:35 2010 -0700
+++ b/src/HOLCF/Domain_Aux.thy	Wed Oct 27 13:54:18 2010 -0700
@@ -71,14 +71,14 @@
 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)
diff -r b283680d8044 -r d065b195ec89 src/HOLCF/Fix.thy
--- a/src/HOLCF/Fix.thy	Wed Oct 27 11:11:35 2010 -0700
+++ b/src/HOLCF/Fix.thy	Wed Oct 27 13:54:18 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 b283680d8044 -r d065b195ec89 src/HOLCF/Lift.thy
--- a/src/HOLCF/Lift.thy	Wed Oct 27 11:11:35 2010 -0700
+++ b/src/HOLCF/Lift.thy	Wed Oct 27 13:54:18 2010 -0700
@@ -114,7 +114,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 b283680d8044 -r d065b195ec89 src/HOLCF/LowerPD.thy
--- a/src/HOLCF/LowerPD.thy	Wed Oct 27 11:11:35 2010 -0700
+++ b/src/HOLCF/LowerPD.thy	Wed Oct 27 13:54:18 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)
diff -r b283680d8044 -r d065b195ec89 src/HOLCF/Pcpodef.thy
--- a/src/HOLCF/Pcpodef.thy	Wed Oct 27 11:11:35 2010 -0700
+++ b/src/HOLCF/Pcpodef.thy	Wed Oct 27 13:54:18 2010 -0700
@@ -235,7 +235,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 +244,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 +258,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 b283680d8044 -r d065b195ec89 src/HOLCF/Product_Cpo.thy
--- a/src/HOLCF/Product_Cpo.thy	Wed Oct 27 11:11:35 2010 -0700
+++ b/src/HOLCF/Product_Cpo.thy	Wed Oct 27 13:54:18 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 b283680d8044 -r d065b195ec89 src/HOLCF/Sprod.thy
--- a/src/HOLCF/Sprod.thy	Wed Oct 27 11:11:35 2010 -0700
+++ b/src/HOLCF/Sprod.thy	Wed Oct 27 13:54:18 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 b283680d8044 -r d065b195ec89 src/HOLCF/Ssum.thy
--- a/src/HOLCF/Ssum.thy	Wed Oct 27 11:11:35 2010 -0700
+++ b/src/HOLCF/Ssum.thy	Wed Oct 27 13:54:18 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>"
diff -r b283680d8044 -r d065b195ec89 src/HOLCF/Tools/Domain/domain_constructors.ML
--- a/src/HOLCF/Tools/Domain/domain_constructors.ML	Wed Oct 27 11:11:35 2010 -0700
+++ b/src/HOLCF/Tools/Domain/domain_constructors.ML	Wed Oct 27 13:54:18 2010 -0700
@@ -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
@@ -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 b283680d8044 -r d065b195ec89 src/HOLCF/Tools/pcpodef.ML
--- a/src/HOLCF/Tools/pcpodef.ML	Wed Oct 27 11:11:35 2010 -0700
+++ b/src/HOLCF/Tools/pcpodef.ML	Wed Oct 27 13:54:18 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 b283680d8044 -r d065b195ec89 src/HOLCF/Tutorial/Domain_ex.thy
--- a/src/HOLCF/Tutorial/Domain_ex.thy	Wed Oct 27 11:11:35 2010 -0700
+++ b/src/HOLCF/Tutorial/Domain_ex.thy	Wed Oct 27 13:54:18 2010 -0700
@@ -116,8 +116,8 @@
 
 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
diff -r b283680d8044 -r d065b195ec89 src/HOLCF/UpperPD.thy
--- a/src/HOLCF/UpperPD.thy	Wed Oct 27 11:11:35 2010 -0700
+++ b/src/HOLCF/UpperPD.thy	Wed Oct 27 13:54:18 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)