# HG changeset patch
# User huffman
# Date 1291653832 28800
# Node ID 0acff85f95c7fe39b2a291cf76185a663841cd62
# Parent  c599955d9806e09f9ae6d2a5bcad1897d681811c
cpodef no longer generates lemma is_lub_foo, since it is redundant with lub_foo

diff -r c599955d9806 -r 0acff85f95c7 src/HOL/HOLCF/Tools/cpodef.ML
--- a/src/HOL/HOLCF/Tools/cpodef.ML	Mon Dec 06 08:30:00 2010 -0800
+++ b/src/HOL/HOLCF/Tools/cpodef.ML	Mon Dec 06 08:43:52 2010 -0800
@@ -9,7 +9,7 @@
 sig
   type cpo_info =
     { below_def: thm, adm: thm, cont_Rep: thm, cont_Abs: thm,
-      is_lub: thm, lub: thm, compact: thm }
+      lub: thm, compact: thm }
   type pcpo_info =
     { Rep_strict: thm, Abs_strict: thm, Rep_bottom_iff: thm, Abs_bottom_iff: thm,
       Rep_defined: thm, Abs_defined: thm }
@@ -45,7 +45,7 @@
 
 type cpo_info =
   { below_def: thm, adm: thm, cont_Rep: thm, cont_Abs: thm,
-    is_lub: thm, lub: thm, compact: thm }
+    lub: thm, compact: thm }
 
 type pcpo_info =
   { Rep_strict: thm, Abs_strict: thm, Rep_bottom_iff: thm, Abs_bottom_iff: thm,
@@ -94,7 +94,6 @@
     fun make thm = Drule.zero_var_indexes (thm OF cpo_thms')
     val cont_Rep = make @{thm typedef_cont_Rep}
     val cont_Abs = make @{thm typedef_cont_Abs}
-    val is_lub = make @{thm typedef_is_lub}
     val lub = make @{thm typedef_lub}
     val compact = make @{thm typedef_compact}
     val (_, thy) =
@@ -104,13 +103,12 @@
         ([((Binding.prefix_name "adm_"      name, admissible'), []),
           ((Binding.prefix_name "cont_" Rep_name, cont_Rep   ), []),
           ((Binding.prefix_name "cont_" Abs_name, cont_Abs   ), []),
-          ((Binding.prefix_name "is_lub_"   name, is_lub     ), []),
           ((Binding.prefix_name "lub_"      name, lub        ), []),
           ((Binding.prefix_name "compact_"  name, compact    ), [])])
       ||> Sign.parent_path
     val cpo_info : cpo_info =
       { below_def = below_def, adm = admissible', cont_Rep = cont_Rep,
-        cont_Abs = cont_Abs, is_lub = is_lub, lub = lub, compact = compact }
+        cont_Abs = cont_Abs, lub = lub, compact = compact }
   in
     (cpo_info, thy)
   end