# HG changeset patch
# User huffman
# Date 1316721319 25200
# Node ID 13efaee97111f8f98f15dec5a0a0df55d22fae05
# Parent  5ff8cd3b1673e1ade93d95cb8742ec4e06fa2e79
discontinued HOLCF legacy theorem names

diff -r 5ff8cd3b1673 -r 13efaee97111 NEWS
--- a/NEWS	Thu Sep 22 17:15:46 2011 +0200
+++ b/NEWS	Thu Sep 22 12:55:19 2011 -0700
@@ -444,6 +444,34 @@
   - Use extended reals instead of positive extended
     reals. INCOMPATIBILITY.
 
+* Session HOLCF: Discontinued legacy theorem names, INCOMPATIBILITY.
+
+  expand_fun_below ~> fun_below_iff
+  below_fun_ext ~> fun_belowI
+  expand_cfun_eq ~> cfun_eq_iff
+  ext_cfun ~> cfun_eqI
+  expand_cfun_below ~> cfun_below_iff
+  below_cfun_ext ~> cfun_belowI
+  monofun_fun_fun ~> fun_belowD
+  monofun_fun_arg ~> monofunE
+  monofun_lub_fun ~> adm_monofun [THEN admD]
+  cont_lub_fun ~> adm_cont [THEN admD]
+  cont2cont_Rep_CFun ~> cont2cont_APP
+  cont_Rep_CFun_app ~> cont_APP_app
+  cont_Rep_CFun_app_app ~> cont_APP_app_app
+  cont_cfun_fun ~> cont_Rep_cfun1 [THEN contE]
+  cont_cfun_arg ~> cont_Rep_cfun2 [THEN contE]
+  contlub_cfun ~> lub_APP [symmetric]
+  contlub_LAM ~> lub_LAM [symmetric]
+  thelubI ~> lub_eqI
+  UU_I ~> bottomI
+  lift_distinct1 ~> lift.distinct(1)
+  lift_distinct2 ~> lift.distinct(2)
+  Def_not_UU ~> lift.distinct(2)
+  Def_inject ~> lift.inject
+  below_UU_iff ~> below_bottom_iff
+  eq_UU_iff ~> eq_bottom_iff
+
 
 *** Document preparation ***
 
diff -r 5ff8cd3b1673 -r 13efaee97111 src/HOL/HOLCF/FOCUS/Fstream.thy
--- a/src/HOL/HOLCF/FOCUS/Fstream.thy	Thu Sep 22 17:15:46 2011 +0200
+++ b/src/HOL/HOLCF/FOCUS/Fstream.thy	Thu Sep 22 12:55:19 2011 -0700
@@ -81,13 +81,13 @@
 lemma fstream_prefix: "a~> s << t ==> ? tt. t = a~> tt &  s << tt"
 apply (cases t)
 apply (cut_tac fscons_not_empty)
-apply (fast dest: eq_UU_iff [THEN iffD2])
+apply (fast dest: bottomI)
 apply (simp add: fscons_def2)
 done
 
 lemma fstream_prefix' [simp]:
         "x << a~> z = (x = <> |  (? y. x = a~> y &  y << z))"
-apply (simp add: fscons_def2 Def_not_UU [THEN stream_prefix'])
+apply (simp add: fscons_def2 lift.distinct(2) [THEN stream_prefix'])
 apply (safe)
 apply (erule_tac [!] contrapos_np)
 prefer 2 apply (fast elim: DefE)
diff -r 5ff8cd3b1673 -r 13efaee97111 src/HOL/HOLCF/HOLCF.thy
--- a/src/HOL/HOLCF/HOLCF.thy	Thu Sep 22 17:15:46 2011 +0200
+++ b/src/HOL/HOLCF/HOLCF.thy	Thu Sep 22 12:55:19 2011 -0700
@@ -13,32 +13,4 @@
 
 default_sort "domain"
 
-text {* Legacy theorem names deprecated after Isabelle2009-2: *}
-
-lemmas expand_fun_below = fun_below_iff
-lemmas below_fun_ext = fun_belowI
-lemmas expand_cfun_eq = cfun_eq_iff
-lemmas ext_cfun = cfun_eqI
-lemmas expand_cfun_below = cfun_below_iff
-lemmas below_cfun_ext = cfun_belowI
-lemmas monofun_fun_fun = fun_belowD
-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
-lemmas cont_cfun_fun = cont_Rep_cfun1 [THEN contE]
-lemmas cont_cfun_arg = cont_Rep_cfun2 [THEN contE]
-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 5ff8cd3b1673 -r 13efaee97111 src/HOL/HOLCF/ex/Dnat.thy
--- a/src/HOL/HOLCF/ex/Dnat.thy	Thu Sep 22 17:15:46 2011 +0200
+++ b/src/HOL/HOLCF/ex/Dnat.thy	Thu Sep 22 12:55:19 2011 -0700
@@ -61,7 +61,7 @@
    apply simp
   apply (rule allI)
   apply (case_tac y)
-    apply (fast intro!: UU_I)
+    apply (fast intro!: bottomI)
    apply (thin_tac "ALL y. dnat << y --> dnat = UU | dnat = y")
    apply simp
   apply (simp (no_asm_simp))