# HG changeset patch
# User huffman
# Date 1294183976 28800
# Node ID 1aa23e9f2c872acd2cf801db3adb326119271116
# Parent  cf5f025bc3c7adbf54715de36534653a61a6a4c6
change some lemma names containing 'UU' to 'bottom'

diff -r cf5f025bc3c7 -r 1aa23e9f2c87 NEWS
--- a/NEWS	Tue Jan 04 15:03:27 2011 -0800
+++ b/NEWS	Tue Jan 04 15:32:56 2011 -0800
@@ -599,6 +599,10 @@
   thelub_cprod    ~> lub_prod
   minimal_cprod   ~> minimal_prod
   inst_cprod_pcpo ~> inst_prod_pcpo
+  UU_I            ~> bottomI
+  compact_UU      ~> compact_bottom
+  deflation_UU    ~> deflation_bottom
+  finite_deflation_UU ~> finite_deflation_bottom
 
 * Many legacy theorem names have been discontinued. INCOMPATIBILITY.
   sq_ord_less_eq_trans ~> below_eq_trans
diff -r cf5f025bc3c7 -r 1aa23e9f2c87 src/HOL/HOLCF/Adm.thy
--- a/src/HOL/HOLCF/Adm.thy	Tue Jan 04 15:03:27 2011 -0800
+++ b/src/HOL/HOLCF/Adm.thy	Tue Jan 04 15:32:56 2011 -0800
@@ -175,7 +175,7 @@
   "\<lbrakk>compact k; cont (\<lambda>x. t x)\<rbrakk> \<Longrightarrow> adm (\<lambda>x. k \<noteq> t x)"
 by (simp add: po_eq_conv)
 
-lemma compact_UU [simp, intro]: "compact \<bottom>"
+lemma compact_bottom [simp, intro]: "compact \<bottom>"
 by (rule compactI, simp)
 
 text {* Any upward-closed predicate is admissible. *}
diff -r cf5f025bc3c7 -r 1aa23e9f2c87 src/HOL/HOLCF/Algebraic.thy
--- a/src/HOL/HOLCF/Algebraic.thy	Tue Jan 04 15:03:27 2011 -0800
+++ b/src/HOL/HOLCF/Algebraic.thy	Tue Jan 04 15:32:56 2011 -0800
@@ -13,7 +13,7 @@
 subsection {* Type constructor for finite deflations *}
 
 typedef (open) 'a fin_defl = "{d::'a \<rightarrow> 'a. finite_deflation d}"
-by (fast intro: finite_deflation_UU)
+by (fast intro: finite_deflation_bottom)
 
 instantiation fin_defl :: (bifinite) below
 begin
@@ -138,14 +138,14 @@
 apply (induct x rule: defl.principal_induct, simp)
 apply (rule defl.principal_mono)
 apply (simp add: below_fin_defl_def)
-apply (simp add: Abs_fin_defl_inverse finite_deflation_UU)
+apply (simp add: Abs_fin_defl_inverse finite_deflation_bottom)
 done
 
 instance defl :: (bifinite) pcpo
 by intro_classes (fast intro: defl_minimal)
 
 lemma inst_defl_pcpo: "\<bottom> = defl_principal (Abs_fin_defl \<bottom>)"
-by (rule defl_minimal [THEN UU_I, symmetric])
+by (rule defl_minimal [THEN bottomI, symmetric])
 
 subsection {* Applying algebraic deflations *}
 
@@ -209,11 +209,11 @@
 apply (subst inst_defl_pcpo)
 apply (subst cast_defl_principal)
 apply (rule Abs_fin_defl_inverse)
-apply (simp add: finite_deflation_UU)
+apply (simp add: finite_deflation_bottom)
 done
 
 lemma cast_strict2 [simp]: "cast\<cdot>A\<cdot>\<bottom> = \<bottom>"
-by (rule cast.below [THEN UU_I])
+by (rule cast.below [THEN bottomI])
 
 subsection {* Deflation combinators *}
 
diff -r cf5f025bc3c7 -r 1aa23e9f2c87 src/HOL/HOLCF/Bifinite.thy
--- a/src/HOL/HOLCF/Bifinite.thy	Tue Jan 04 15:03:27 2011 -0800
+++ b/src/HOL/HOLCF/Bifinite.thy	Tue Jan 04 15:32:56 2011 -0800
@@ -253,7 +253,7 @@
 qed
 
 lemma approx_chain_unit: "approx_chain (\<bottom> :: nat \<Rightarrow> unit \<rightarrow> unit)"
-by (simp add: approx_chain_def cfun_eq_iff finite_deflation_UU)
+by (simp add: approx_chain_def cfun_eq_iff finite_deflation_bottom)
 
 instance unit :: bifinite
   by default (fast intro!: approx_chain_unit)
diff -r cf5f025bc3c7 -r 1aa23e9f2c87 src/HOL/HOLCF/Cfun.thy
--- a/src/HOL/HOLCF/Cfun.thy	Tue Jan 04 15:03:27 2011 -0800
+++ b/src/HOL/HOLCF/Cfun.thy	Tue Jan 04 15:32:56 2011 -0800
@@ -92,20 +92,20 @@
 
 subsection {* Continuous function space is pointed *}
 
-lemma UU_cfun: "\<bottom> \<in> cfun"
+lemma bottom_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)
 
 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 bottom_cfun])
 
 lemmas Rep_cfun_strict =
-  typedef_Rep_strict [OF type_definition_cfun below_cfun_def UU_cfun]
+  typedef_Rep_strict [OF type_definition_cfun below_cfun_def bottom_cfun]
 
 lemmas Abs_cfun_strict =
-  typedef_Abs_strict [OF type_definition_cfun below_cfun_def UU_cfun]
+  typedef_Abs_strict [OF type_definition_cfun below_cfun_def bottom_cfun]
 
 text {* function application is strict in its first argument *}
 
@@ -261,7 +261,7 @@
 text {* strictness *}
 
 lemma strictI: "f\<cdot>x = \<bottom> \<Longrightarrow> f\<cdot>\<bottom> = \<bottom>"
-apply (rule UU_I)
+apply (rule bottomI)
 apply (erule subst)
 apply (rule minimal [THEN monofun_cfun_arg])
 done
@@ -364,7 +364,7 @@
 
 lemma retraction_strict:
   "\<forall>x. f\<cdot>(g\<cdot>x) = x \<Longrightarrow> f\<cdot>\<bottom> = \<bottom>"
-apply (rule UU_I)
+apply (rule bottomI)
 apply (drule_tac x="\<bottom>" in spec)
 apply (erule subst)
 apply (rule monofun_cfun_arg)
@@ -406,7 +406,7 @@
   "f\<cdot>x = (c::'b::flat) \<Longrightarrow> f\<cdot>\<bottom> = \<bottom> \<or> (\<forall>z. f\<cdot>z = c)"
 apply (case_tac "f\<cdot>x = \<bottom>")
 apply (rule disjI1)
-apply (rule UU_I)
+apply (rule bottomI)
 apply (erule_tac t="\<bottom>" in subst)
 apply (rule minimal [THEN monofun_cfun_arg])
 apply clarify
diff -r cf5f025bc3c7 -r 1aa23e9f2c87 src/HOL/HOLCF/ConvexPD.thy
--- a/src/HOL/HOLCF/ConvexPD.thy	Tue Jan 04 15:03:27 2011 -0800
+++ b/src/HOL/HOLCF/ConvexPD.thy	Tue Jan 04 15:32:56 2011 -0800
@@ -161,7 +161,7 @@
 by intro_classes (fast intro: convex_pd_minimal)
 
 lemma inst_convex_pd_pcpo: "\<bottom> = convex_principal (PDUnit compact_bot)"
-by (rule convex_pd_minimal [THEN UU_I, symmetric])
+by (rule convex_pd_minimal [THEN bottomI, symmetric])
 
 
 subsection {* Monadic unit and plus *}
diff -r cf5f025bc3c7 -r 1aa23e9f2c87 src/HOL/HOLCF/Cpodef.thy
--- a/src/HOL/HOLCF/Cpodef.thy	Tue Jan 04 15:03:27 2011 -0800
+++ b/src/HOL/HOLCF/Cpodef.thy	Tue Jan 04 15:32:56 2011 -0800
@@ -203,9 +203,9 @@
   fixes Abs :: "'a::pcpo \<Rightarrow> 'b::cpo"
   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"
+    and bottom_in_A: "\<bottom> \<in> A"
   shows "OFCLASS('b, pcpo_class)"
-by (rule typedef_pcpo_generic [OF type below UU_in_A], rule minimal)
+by (rule typedef_pcpo_generic [OF type below bottom_in_A], rule minimal)
 
 subsubsection {* Strictness of \emph{Rep} and \emph{Abs} *}
 
@@ -217,36 +217,36 @@
 theorem typedef_Abs_strict:
   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"
+    and bottom_in_A: "\<bottom> \<in> A"
   shows "Abs \<bottom> = \<bottom>"
- apply (rule UU_I, unfold below)
- apply (simp add: type_definition.Abs_inverse [OF type UU_in_A])
+ apply (rule bottomI, unfold below)
+ apply (simp add: type_definition.Abs_inverse [OF type bottom_in_A])
 done
 
 theorem typedef_Rep_strict:
   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"
+    and bottom_in_A: "\<bottom> \<in> A"
   shows "Rep \<bottom> = \<bottom>"
- apply (rule typedef_Abs_strict [OF type below UU_in_A, THEN subst])
- apply (rule type_definition.Abs_inverse [OF type UU_in_A])
+ apply (rule typedef_Abs_strict [OF type below bottom_in_A, THEN subst])
+ apply (rule type_definition.Abs_inverse [OF type bottom_in_A])
 done
 
 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"
+    and bottom_in_A: "\<bottom> \<in> A"
   shows "x \<in> A \<Longrightarrow> (Abs x = \<bottom>) = (x = \<bottom>)"
- apply (rule typedef_Abs_strict [OF type below UU_in_A, THEN subst])
- apply (simp add: type_definition.Abs_inject [OF type] UU_in_A)
+ apply (rule typedef_Abs_strict [OF type below bottom_in_A, THEN subst])
+ apply (simp add: type_definition.Abs_inject [OF type] bottom_in_A)
 done
 
 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"
+    and bottom_in_A: "\<bottom> \<in> A"
   shows "(Rep x = \<bottom>) = (x = \<bottom>)"
- apply (rule typedef_Rep_strict [OF type below UU_in_A, THEN subst])
+ apply (rule typedef_Rep_strict [OF type below bottom_in_A, THEN subst])
  apply (simp add: type_definition.Rep_inject [OF type])
 done
 
@@ -256,12 +256,12 @@
   fixes Abs :: "'a::flat \<Rightarrow> 'b::pcpo"
   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"
+    and bottom_in_A: "\<bottom> \<in> A"
   shows "OFCLASS('b, flat_class)"
  apply (intro_classes)
  apply (unfold below)
  apply (simp add: type_definition.Rep_inject [OF type, symmetric])
- apply (simp add: typedef_Rep_strict [OF type below UU_in_A])
+ apply (simp add: typedef_Rep_strict [OF type below bottom_in_A])
  apply (simp add: ax_flat)
 done
 
diff -r cf5f025bc3c7 -r 1aa23e9f2c87 src/HOL/HOLCF/Deflation.thy
--- a/src/HOL/HOLCF/Deflation.thy	Tue Jan 04 15:03:27 2011 -0800
+++ b/src/HOL/HOLCF/Deflation.thy	Tue Jan 04 15:32:56 2011 -0800
@@ -56,7 +56,7 @@
 end
 
 lemma deflation_strict: "deflation d \<Longrightarrow> d\<cdot>\<bottom> = \<bottom>"
-by (rule deflation.below [THEN UU_I])
+by (rule deflation.below [THEN bottomI])
 
 lemma adm_deflation: "adm (\<lambda>d. deflation d)"
 by (simp add: deflation_def)
@@ -64,7 +64,7 @@
 lemma deflation_ID: "deflation ID"
 by (simp add: deflation.intro)
 
-lemma deflation_UU: "deflation \<bottom>"
+lemma deflation_bottom: "deflation \<bottom>"
 by (simp add: deflation.intro)
 
 lemma deflation_below_iff:
@@ -160,7 +160,7 @@
   "finite_deflation d \<Longrightarrow> deflation d"
 unfolding finite_deflation_def by simp
 
-lemma finite_deflation_UU: "finite_deflation \<bottom>"
+lemma finite_deflation_bottom: "finite_deflation \<bottom>"
 by default simp_all
 
 
diff -r cf5f025bc3c7 -r 1aa23e9f2c87 src/HOL/HOLCF/Domain_Aux.thy
--- a/src/HOL/HOLCF/Domain_Aux.thy	Tue Jan 04 15:03:27 2011 -0800
+++ b/src/HOL/HOLCF/Domain_Aux.thy	Tue Jan 04 15:32:56 2011 -0800
@@ -52,7 +52,7 @@
   have "\<bottom> \<sqsubseteq> rep\<cdot>\<bottom>" ..
   then have "abs\<cdot>\<bottom> \<sqsubseteq> abs\<cdot>(rep\<cdot>\<bottom>)" by (rule monofun_cfun_arg)
   then have "abs\<cdot>\<bottom> \<sqsubseteq> \<bottom>" by simp
-  then show ?thesis by (rule UU_I)
+  then show ?thesis by (rule bottomI)
 qed
 
 lemma rep_strict: "rep\<cdot>\<bottom> = \<bottom>"
diff -r cf5f025bc3c7 -r 1aa23e9f2c87 src/HOL/HOLCF/Fix.thy
--- a/src/HOL/HOLCF/Fix.thy	Tue Jan 04 15:03:27 2011 -0800
+++ b/src/HOL/HOLCF/Fix.thy	Tue Jan 04 15:32:56 2011 -0800
@@ -122,7 +122,7 @@
 apply (rule iffI)
 apply (erule subst)
 apply (rule fix_eq [symmetric])
-apply (erule fix_least [THEN UU_I])
+apply (erule fix_least [THEN bottomI])
 done
 
 lemma fix_strict: "F\<cdot>\<bottom> = \<bottom> \<Longrightarrow> fix\<cdot>F = \<bottom>"
diff -r cf5f025bc3c7 -r 1aa23e9f2c87 src/HOL/HOLCF/Fun_Cpo.thy
--- a/src/HOL/HOLCF/Fun_Cpo.thy	Tue Jan 04 15:03:27 2011 -0800
+++ b/src/HOL/HOLCF/Fun_Cpo.thy	Tue Jan 04 15:32:56 2011 -0800
@@ -96,13 +96,13 @@
 by default (fast intro: minimal_fun)
 
 lemma inst_fun_pcpo: "\<bottom> = (\<lambda>x. \<bottom>)"
-by (rule minimal_fun [THEN UU_I, symmetric])
+by (rule minimal_fun [THEN bottomI, symmetric])
 
 lemma app_strict [simp]: "\<bottom> x = \<bottom>"
 by (simp add: inst_fun_pcpo)
 
 lemma lambda_strict: "(\<lambda>x. \<bottom>) = \<bottom>"
-by (rule UU_I, rule minimal_fun)
+by (rule bottomI, rule minimal_fun)
 
 subsection {* Propagation of monotonicity and continuity *}
 
diff -r cf5f025bc3c7 -r 1aa23e9f2c87 src/HOL/HOLCF/HOLCF.thy
--- a/src/HOL/HOLCF/HOLCF.thy	Tue Jan 04 15:03:27 2011 -0800
+++ b/src/HOL/HOLCF/HOLCF.thy	Tue Jan 04 15:32:56 2011 -0800
@@ -35,5 +35,12 @@
 lemmas contlub_cfun = lub_APP [symmetric]
 lemmas contlub_LAM = lub_LAM [symmetric]
 lemmas thelubI = lub_eqI
+lemmas UU_I = bottomI
+lemmas lift_distinct1 = lift.distinct(1)
+lemmas lift_distinct2 = lift.distinct(2)
+lemmas Def_not_UU = lift.distinct(2)
+lemmas Def_inject = lift.inject
+lemmas below_UU_iff = below_bottom_iff
+lemmas eq_UU_iff = eq_bottom_iff
 
 end
diff -r cf5f025bc3c7 -r 1aa23e9f2c87 src/HOL/HOLCF/Lift.thy
--- a/src/HOL/HOLCF/Lift.thy	Tue Jan 04 15:03:27 2011 -0800
+++ b/src/HOL/HOLCF/Lift.thy	Tue Jan 04 15:32:56 2011 -0800
@@ -32,13 +32,7 @@
 rep_datatype "\<bottom>\<Colon>'a lift" Def
   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)
-lemmas Def_not_UU = lift.distinct(2)
-lemmas Def_inject = lift.inject
-
-
-text {* @{term UU} and @{term Def} *}
+text {* @{term bottom} and @{term Def} *}
 
 lemma not_Undef_is_Def: "(x \<noteq> \<bottom>) = (\<exists>y. x = Def y)"
   by (cases x) simp_all
@@ -47,7 +41,7 @@
   by (cases x) simp_all
 
 text {*
-  For @{term "x ~= UU"} in assumptions @{text defined} replaces @{text
+  For @{term "x ~= \<bottom>"} in assumptions @{text defined} replaces @{text
   x} by @{text "Def a"} in conclusion. *}
 
 method_setup defined = {*
diff -r cf5f025bc3c7 -r 1aa23e9f2c87 src/HOL/HOLCF/LowerPD.thy
--- a/src/HOL/HOLCF/LowerPD.thy	Tue Jan 04 15:03:27 2011 -0800
+++ b/src/HOL/HOLCF/LowerPD.thy	Tue Jan 04 15:32:56 2011 -0800
@@ -116,7 +116,7 @@
 by intro_classes (fast intro: lower_pd_minimal)
 
 lemma inst_lower_pd_pcpo: "\<bottom> = lower_principal (PDUnit compact_bot)"
-by (rule lower_pd_minimal [THEN UU_I, symmetric])
+by (rule lower_pd_minimal [THEN bottomI, symmetric])
 
 
 subsection {* Monadic unit and plus *}
@@ -240,8 +240,8 @@
 lemma lower_plus_bottom_iff [simp]:
   "xs \<union>\<flat> ys = \<bottom> \<longleftrightarrow> xs = \<bottom> \<and> ys = \<bottom>"
 apply safe
-apply (rule UU_I, erule subst, rule lower_plus_below1)
-apply (rule UU_I, erule subst, rule lower_plus_below2)
+apply (rule bottomI, erule subst, rule lower_plus_below1)
+apply (rule bottomI, erule subst, rule lower_plus_below2)
 apply (rule lower_plus_absorb)
 done
 
diff -r cf5f025bc3c7 -r 1aa23e9f2c87 src/HOL/HOLCF/Pcpo.thy
--- a/src/HOL/HOLCF/Pcpo.thy	Tue Jan 04 15:03:27 2011 -0800
+++ b/src/HOL/HOLCF/Pcpo.thy	Tue Jan 04 15:32:56 2011 -0800
@@ -180,17 +180,17 @@
 
 text {* useful lemmas about @{term \<bottom>} *}
 
-lemma below_UU_iff [simp]: "(x \<sqsubseteq> \<bottom>) = (x = \<bottom>)"
+lemma below_bottom_iff [simp]: "(x \<sqsubseteq> \<bottom>) = (x = \<bottom>)"
 by (simp add: po_eq_conv)
 
-lemma eq_UU_iff: "(x = \<bottom>) = (x \<sqsubseteq> \<bottom>)"
+lemma eq_bottom_iff: "(x = \<bottom>) = (x \<sqsubseteq> \<bottom>)"
 by simp
 
-lemma UU_I: "x \<sqsubseteq> \<bottom> \<Longrightarrow> x = \<bottom>"
-by (subst eq_UU_iff)
+lemma bottomI: "x \<sqsubseteq> \<bottom> \<Longrightarrow> x = \<bottom>"
+by (subst eq_bottom_iff)
 
 lemma lub_eq_bottom_iff: "chain Y \<Longrightarrow> (\<Squnion>i. Y i) = \<bottom> \<longleftrightarrow> (\<forall>i. Y i = \<bottom>)"
-by (simp only: eq_UU_iff lub_below_iff)
+by (simp only: eq_bottom_iff lub_below_iff)
 
 lemma chain_UU_I: "\<lbrakk>chain Y; (\<Squnion>i. Y i) = \<bottom>\<rbrakk> \<Longrightarrow> \<forall>i. Y i = \<bottom>"
 by (simp add: lub_eq_bottom_iff)
@@ -202,7 +202,7 @@
   by (blast intro: chain_UU_I_inverse)
 
 lemma notUU_I: "\<lbrakk>x \<sqsubseteq> y; x \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> y \<noteq> \<bottom>"
-  by (blast intro: UU_I)
+  by (blast intro: bottomI)
 
 end
 
diff -r cf5f025bc3c7 -r 1aa23e9f2c87 src/HOL/HOLCF/Product_Cpo.thy
--- a/src/HOL/HOLCF/Product_Cpo.thy	Tue Jan 04 15:03:27 2011 -0800
+++ b/src/HOL/HOLCF/Product_Cpo.thy	Tue Jan 04 15:32:56 2011 -0800
@@ -155,7 +155,7 @@
 by intro_classes (fast intro: minimal_prod)
 
 lemma inst_prod_pcpo: "\<bottom> = (\<bottom>, \<bottom>)"
-by (rule minimal_prod [THEN UU_I, symmetric])
+by (rule minimal_prod [THEN bottomI, symmetric])
 
 lemma Pair_bottom_iff [simp]: "(x, y) = \<bottom> \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>"
 unfolding inst_prod_pcpo by simp
diff -r cf5f025bc3c7 -r 1aa23e9f2c87 src/HOL/HOLCF/Sprod.thy
--- a/src/HOL/HOLCF/Sprod.thy	Tue Jan 04 15:03:27 2011 -0800
+++ b/src/HOL/HOLCF/Sprod.thy	Tue Jan 04 15:32:56 2011 -0800
@@ -117,7 +117,7 @@
   "\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>; (:x, y:) = (:a, b:)\<rbrakk> \<Longrightarrow> x = a \<and> y = b"
 by (rule spair_eq [THEN iffD1])
 
-lemma inst_sprod_pcpo2: "UU = (:UU,UU:)"
+lemma inst_sprod_pcpo2: "\<bottom> = (:\<bottom>, \<bottom>:)"
 by simp
 
 lemma sprodE2: "(\<And>x y. p = (:x, y:) \<Longrightarrow> Q) \<Longrightarrow> Q"
diff -r cf5f025bc3c7 -r 1aa23e9f2c87 src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML
--- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Tue Jan 04 15:03:27 2011 -0800
+++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Tue Jan 04 15:32:56 2011 -0800
@@ -325,7 +325,7 @@
           @{thms adm_conj adm_subst [OF _ adm_deflation]
                  cont2cont_fst cont2cont_snd cont_id}
         val bottom_rules =
-          @{thms fst_strict snd_strict deflation_UU simp_thms}
+          @{thms fst_strict snd_strict deflation_bottom simp_thms}
         val tuple_rules =
           @{thms split_def fst_conv snd_conv}
         val deflation_rules =
diff -r cf5f025bc3c7 -r 1aa23e9f2c87 src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML
--- a/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML	Tue Jan 04 15:03:27 2011 -0800
+++ b/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML	Tue Jan 04 15:32:56 2011 -0800
@@ -330,7 +330,7 @@
           @{thms adm_conj adm_subst [OF _ adm_deflation]
                  cont2cont_fst cont2cont_snd cont_id}
         val bottom_rules =
-          take_0_thms @ @{thms deflation_UU simp_thms}
+          take_0_thms @ @{thms deflation_bottom simp_thms}
         val deflation_rules =
           @{thms conjI deflation_ID}
           @ deflation_abs_rep_thms
diff -r cf5f025bc3c7 -r 1aa23e9f2c87 src/HOL/HOLCF/Universal.thy
--- a/src/HOL/HOLCF/Universal.thy	Tue Jan 04 15:03:27 2011 -0800
+++ b/src/HOL/HOLCF/Universal.thy	Tue Jan 04 15:32:56 2011 -0800
@@ -242,7 +242,7 @@
 by intro_classes (fast intro: udom_minimal)
 
 lemma inst_udom_pcpo: "\<bottom> = udom_principal 0"
-by (rule udom_minimal [THEN UU_I, symmetric])
+by (rule udom_minimal [THEN bottomI, symmetric])
 
 
 subsection {* Compact bases of domains *}
diff -r cf5f025bc3c7 -r 1aa23e9f2c87 src/HOL/HOLCF/Up.thy
--- a/src/HOL/HOLCF/Up.thy	Tue Jan 04 15:03:27 2011 -0800
+++ b/src/HOL/HOLCF/Up.thy	Tue Jan 04 15:32:56 2011 -0800
@@ -127,7 +127,7 @@
 
 text {* for compatibility with old HOLCF-Version *}
 lemma inst_up_pcpo: "\<bottom> = Ibottom"
-by (rule minimal_up [THEN UU_I, symmetric])
+by (rule minimal_up [THEN bottomI, symmetric])
 
 subsection {* Continuity of \emph{Iup} and \emph{Ifup} *}
 
diff -r cf5f025bc3c7 -r 1aa23e9f2c87 src/HOL/HOLCF/UpperPD.thy
--- a/src/HOL/HOLCF/UpperPD.thy	Tue Jan 04 15:03:27 2011 -0800
+++ b/src/HOL/HOLCF/UpperPD.thy	Tue Jan 04 15:32:56 2011 -0800
@@ -114,7 +114,7 @@
 by intro_classes (fast intro: upper_pd_minimal)
 
 lemma inst_upper_pd_pcpo: "\<bottom> = upper_principal (PDUnit compact_bot)"
-by (rule upper_pd_minimal [THEN UU_I, symmetric])
+by (rule upper_pd_minimal [THEN bottomI, symmetric])
 
 
 subsection {* Monadic unit and plus *}
@@ -233,10 +233,10 @@
 by (simp add: inst_upper_pd_pcpo)
 
 lemma upper_plus_strict1 [simp]: "\<bottom> \<union>\<sharp> ys = \<bottom>"
-by (rule UU_I, rule upper_plus_below1)
+by (rule bottomI, rule upper_plus_below1)
 
 lemma upper_plus_strict2 [simp]: "xs \<union>\<sharp> \<bottom> = \<bottom>"
-by (rule UU_I, rule upper_plus_below2)
+by (rule bottomI, rule upper_plus_below2)
 
 lemma upper_unit_bottom_iff [simp]: "{x}\<sharp> = \<bottom> \<longleftrightarrow> x = \<bottom>"
 unfolding upper_unit_strict [symmetric] by (rule upper_unit_eq_iff)