discontinued HOLCF legacy theorem names
authorhuffman
Thu Sep 22 12:55:19 2011 -0700 (2011-09-22)
changeset 4504913efaee97111
parent 45046 5ff8cd3b1673
child 45050 f65593159ee8
discontinued HOLCF legacy theorem names
NEWS
src/HOL/HOLCF/FOCUS/Fstream.thy
src/HOL/HOLCF/HOLCF.thy
src/HOL/HOLCF/ex/Dnat.thy
     1.1 --- a/NEWS	Thu Sep 22 17:15:46 2011 +0200
     1.2 +++ b/NEWS	Thu Sep 22 12:55:19 2011 -0700
     1.3 @@ -444,6 +444,34 @@
     1.4    - Use extended reals instead of positive extended
     1.5      reals. INCOMPATIBILITY.
     1.6  
     1.7 +* Session HOLCF: Discontinued legacy theorem names, INCOMPATIBILITY.
     1.8 +
     1.9 +  expand_fun_below ~> fun_below_iff
    1.10 +  below_fun_ext ~> fun_belowI
    1.11 +  expand_cfun_eq ~> cfun_eq_iff
    1.12 +  ext_cfun ~> cfun_eqI
    1.13 +  expand_cfun_below ~> cfun_below_iff
    1.14 +  below_cfun_ext ~> cfun_belowI
    1.15 +  monofun_fun_fun ~> fun_belowD
    1.16 +  monofun_fun_arg ~> monofunE
    1.17 +  monofun_lub_fun ~> adm_monofun [THEN admD]
    1.18 +  cont_lub_fun ~> adm_cont [THEN admD]
    1.19 +  cont2cont_Rep_CFun ~> cont2cont_APP
    1.20 +  cont_Rep_CFun_app ~> cont_APP_app
    1.21 +  cont_Rep_CFun_app_app ~> cont_APP_app_app
    1.22 +  cont_cfun_fun ~> cont_Rep_cfun1 [THEN contE]
    1.23 +  cont_cfun_arg ~> cont_Rep_cfun2 [THEN contE]
    1.24 +  contlub_cfun ~> lub_APP [symmetric]
    1.25 +  contlub_LAM ~> lub_LAM [symmetric]
    1.26 +  thelubI ~> lub_eqI
    1.27 +  UU_I ~> bottomI
    1.28 +  lift_distinct1 ~> lift.distinct(1)
    1.29 +  lift_distinct2 ~> lift.distinct(2)
    1.30 +  Def_not_UU ~> lift.distinct(2)
    1.31 +  Def_inject ~> lift.inject
    1.32 +  below_UU_iff ~> below_bottom_iff
    1.33 +  eq_UU_iff ~> eq_bottom_iff
    1.34 +
    1.35  
    1.36  *** Document preparation ***
    1.37  
     2.1 --- a/src/HOL/HOLCF/FOCUS/Fstream.thy	Thu Sep 22 17:15:46 2011 +0200
     2.2 +++ b/src/HOL/HOLCF/FOCUS/Fstream.thy	Thu Sep 22 12:55:19 2011 -0700
     2.3 @@ -81,13 +81,13 @@
     2.4  lemma fstream_prefix: "a~> s << t ==> ? tt. t = a~> tt &  s << tt"
     2.5  apply (cases t)
     2.6  apply (cut_tac fscons_not_empty)
     2.7 -apply (fast dest: eq_UU_iff [THEN iffD2])
     2.8 +apply (fast dest: bottomI)
     2.9  apply (simp add: fscons_def2)
    2.10  done
    2.11  
    2.12  lemma fstream_prefix' [simp]:
    2.13          "x << a~> z = (x = <> |  (? y. x = a~> y &  y << z))"
    2.14 -apply (simp add: fscons_def2 Def_not_UU [THEN stream_prefix'])
    2.15 +apply (simp add: fscons_def2 lift.distinct(2) [THEN stream_prefix'])
    2.16  apply (safe)
    2.17  apply (erule_tac [!] contrapos_np)
    2.18  prefer 2 apply (fast elim: DefE)
     3.1 --- a/src/HOL/HOLCF/HOLCF.thy	Thu Sep 22 17:15:46 2011 +0200
     3.2 +++ b/src/HOL/HOLCF/HOLCF.thy	Thu Sep 22 12:55:19 2011 -0700
     3.3 @@ -13,32 +13,4 @@
     3.4  
     3.5  default_sort "domain"
     3.6  
     3.7 -text {* Legacy theorem names deprecated after Isabelle2009-2: *}
     3.8 -
     3.9 -lemmas expand_fun_below = fun_below_iff
    3.10 -lemmas below_fun_ext = fun_belowI
    3.11 -lemmas expand_cfun_eq = cfun_eq_iff
    3.12 -lemmas ext_cfun = cfun_eqI
    3.13 -lemmas expand_cfun_below = cfun_below_iff
    3.14 -lemmas below_cfun_ext = cfun_belowI
    3.15 -lemmas monofun_fun_fun = fun_belowD
    3.16 -lemmas monofun_fun_arg = monofunE
    3.17 -lemmas monofun_lub_fun = adm_monofun [THEN admD]
    3.18 -lemmas cont_lub_fun = adm_cont [THEN admD]
    3.19 -lemmas cont2cont_Rep_CFun = cont2cont_APP
    3.20 -lemmas cont_Rep_CFun_app = cont_APP_app
    3.21 -lemmas cont_Rep_CFun_app_app = cont_APP_app_app
    3.22 -lemmas cont_cfun_fun = cont_Rep_cfun1 [THEN contE]
    3.23 -lemmas cont_cfun_arg = cont_Rep_cfun2 [THEN contE]
    3.24 -lemmas contlub_cfun = lub_APP [symmetric]
    3.25 -lemmas contlub_LAM = lub_LAM [symmetric]
    3.26 -lemmas thelubI = lub_eqI
    3.27 -lemmas UU_I = bottomI
    3.28 -lemmas lift_distinct1 = lift.distinct(1)
    3.29 -lemmas lift_distinct2 = lift.distinct(2)
    3.30 -lemmas Def_not_UU = lift.distinct(2)
    3.31 -lemmas Def_inject = lift.inject
    3.32 -lemmas below_UU_iff = below_bottom_iff
    3.33 -lemmas eq_UU_iff = eq_bottom_iff
    3.34 -
    3.35  end
     4.1 --- a/src/HOL/HOLCF/ex/Dnat.thy	Thu Sep 22 17:15:46 2011 +0200
     4.2 +++ b/src/HOL/HOLCF/ex/Dnat.thy	Thu Sep 22 12:55:19 2011 -0700
     4.3 @@ -61,7 +61,7 @@
     4.4     apply simp
     4.5    apply (rule allI)
     4.6    apply (case_tac y)
     4.7 -    apply (fast intro!: UU_I)
     4.8 +    apply (fast intro!: bottomI)
     4.9     apply (thin_tac "ALL y. dnat << y --> dnat = UU | dnat = y")
    4.10     apply simp
    4.11    apply (simp (no_asm_simp))