1.1 --- a/src/HOLCF/Cfun.thy	Sat Nov 27 12:38:02 2010 -0800
     1.2 +++ b/src/HOLCF/Cfun.thy	Sat Nov 27 12:55:12 2010 -0800
     1.3 @@ -264,7 +264,7 @@
     1.4  lemma contlub_LAM:
     1.5    "\<lbrakk>\<And>x. chain (\<lambda>i. F i x); \<And>i. cont (\<lambda>x. F i x)\<rbrakk>
     1.6      \<Longrightarrow> (\<Lambda> x. \<Squnion>i. F i x) = (\<Squnion>i. \<Lambda> x. F i x)"
     1.7 -apply (simp add: thelub_cfun)
     1.8 +apply (simp add: lub_cfun)
     1.9  apply (simp add: Abs_cfun_inverse2)
    1.10  apply (simp add: thelub_fun ch2ch_lambda)
    1.11  done

     2.1 --- a/src/HOLCF/Pcpodef.thy	Sat Nov 27 12:38:02 2010 -0800
     2.2 +++ b/src/HOLCF/Pcpodef.thy	Sat Nov 27 12:55:12 2010 -0800
     2.3 @@ -91,7 +91,7 @@
     2.4   apply (rule type_definition.Rep [OF type])
     2.5  done
     2.6  
     2.7 -theorem typedef_lub:
     2.8 +theorem typedef_is_lub:
     2.9    fixes Abs :: "'a::cpo \<Rightarrow> 'b::po"
    2.10    assumes type: "type_definition Rep Abs A"
    2.11      and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
    2.12 @@ -107,7 +107,7 @@
    2.13      by (rule typedef_is_lubI [OF below])
    2.14  qed
    2.15  
    2.16 -lemmas typedef_thelub = typedef_lub [THEN thelubI, standard]
    2.17 +lemmas typedef_lub = typedef_is_lub [THEN thelubI, standard]
    2.18  
    2.19  theorem typedef_cpo:
    2.20    fixes Abs :: "'a::cpo \<Rightarrow> 'b::po"
    2.21 @@ -118,7 +118,7 @@
    2.22  proof
    2.23    fix S::"nat \<Rightarrow> 'b" assume "chain S"
    2.24    hence "range S <<| Abs (\<Squnion>i. Rep (S i))"
    2.25 -    by (rule typedef_lub [OF type below adm])
    2.26 +    by (rule typedef_is_lub [OF type below adm])
    2.27    thus "\<exists>x. range S <<| x" ..
    2.28  qed
    2.29  
    2.30 @@ -133,7 +133,7 @@
    2.31      and adm: "adm (\<lambda>x. x \<in> A)"
    2.32    shows "cont Rep"
    2.33   apply (rule contI)
    2.34 - apply (simp only: typedef_thelub [OF type below adm])
    2.35 + apply (simp only: typedef_lub [OF type below adm])
    2.36   apply (simp only: Abs_inverse_lub_Rep [OF type below adm])
    2.37   apply (rule cpo_lubI)
    2.38   apply (erule ch2ch_Rep [OF below])

     3.1 --- a/src/HOLCF/Tools/pcpodef.ML	Sat Nov 27 12:38:02 2010 -0800
     3.2 +++ b/src/HOLCF/Tools/pcpodef.ML	Sat Nov 27 12:55:12 2010 -0800
     3.3 @@ -9,7 +9,7 @@
     3.4  sig
     3.5    type cpo_info =
     3.6      { below_def: thm, adm: thm, cont_Rep: thm, cont_Abs: thm,
     3.7 -      lub: thm, thelub: thm, compact: thm }
     3.8 +      is_lub: thm, lub: thm, compact: thm }
     3.9    type pcpo_info =
    3.10      { Rep_strict: thm, Abs_strict: thm, Rep_bottom_iff: thm, Abs_bottom_iff: thm,
    3.11        Rep_defined: thm, Abs_defined: thm }
    3.12 @@ -45,7 +45,7 @@
    3.13  
    3.14  type cpo_info =
    3.15    { below_def: thm, adm: thm, cont_Rep: thm, cont_Abs: thm,
    3.16 -    lub: thm, thelub: thm, compact: thm }
    3.17 +    is_lub: thm, lub: thm, compact: thm }
    3.18  
    3.19  type pcpo_info =
    3.20    { Rep_strict: thm, Abs_strict: thm, Rep_bottom_iff: thm, Abs_bottom_iff: thm,
    3.21 @@ -94,8 +94,8 @@
    3.22      fun make thm = Drule.zero_var_indexes (thm OF cpo_thms');
    3.23      val cont_Rep = make @{thm typedef_cont_Rep};
    3.24      val cont_Abs = make @{thm typedef_cont_Abs};
    3.25 +    val is_lub = make @{thm typedef_is_lub};
    3.26      val lub = make @{thm typedef_lub};
    3.27 -    val thelub = make @{thm typedef_thelub};
    3.28      val compact = make @{thm typedef_compact};
    3.29      val (_, thy) =
    3.30        thy
    3.31 @@ -104,13 +104,13 @@
    3.32          ([((Binding.prefix_name "adm_"      name, admissible'), []),
    3.33            ((Binding.prefix_name "cont_" Rep_name, cont_Rep   ), []),
    3.34            ((Binding.prefix_name "cont_" Abs_name, cont_Abs   ), []),
    3.35 +          ((Binding.prefix_name "is_lub_"   name, is_lub     ), []),
    3.36            ((Binding.prefix_name "lub_"      name, lub        ), []),
    3.37 -          ((Binding.prefix_name "thelub_"   name, thelub     ), []),
    3.38            ((Binding.prefix_name "compact_"  name, compact    ), [])])
    3.39        ||> Sign.parent_path;
    3.40      val cpo_info : cpo_info =
    3.41        { below_def = below_def, adm = admissible', cont_Rep = cont_Rep,
    3.42 -        cont_Abs = cont_Abs, lub = lub, thelub = thelub, compact = compact };
    3.43 +        cont_Abs = cont_Abs, is_lub = is_lub, lub = lub, compact = compact };
    3.44    in
    3.45      (cpo_info, thy)
    3.46    end;