src/HOLCF/HOLCF.thy
author huffman
Tue Oct 12 06:20:05 2010 -0700 (2010-10-12)
changeset 40006 116e94f9543b
parent 40002 c5b5f7a3a3b1
child 40011 b974cf829099
permissions -rw-r--r--
remove unneeded lemmas from Fun_Cpo.thy
     1 (*  Title:      HOLCF/HOLCF.thy
     2     Author:     Franz Regensburger
     3 
     4 HOLCF -- a semantic extension of HOL by the LCF logic.
     5 *)
     6 
     7 theory HOLCF
     8 imports
     9   Main
    10   Domain
    11   Powerdomains
    12 begin
    13 
    14 default_sort pcpo
    15 
    16 ML {* path_add "~~/src/HOLCF/Library" *}
    17 
    18 text {* Legacy theorem names deprecated after Isabelle2009-2: *}
    19 
    20 lemmas expand_fun_below = fun_below_iff
    21 lemmas below_fun_ext = fun_belowI
    22 lemmas expand_cfun_eq = cfun_eq_iff
    23 lemmas ext_cfun = cfun_eqI
    24 lemmas expand_cfun_below = cfun_below_iff
    25 lemmas below_cfun_ext = cfun_belowI
    26 
    27 text {* Older legacy theorem names: *}
    28 
    29 lemmas sq_ord_less_eq_trans = below_eq_trans
    30 lemmas sq_ord_eq_less_trans = eq_below_trans
    31 lemmas refl_less = below_refl
    32 lemmas trans_less = below_trans
    33 lemmas antisym_less = below_antisym
    34 lemmas antisym_less_inverse = below_antisym_inverse
    35 lemmas box_less = box_below
    36 lemmas rev_trans_less = rev_below_trans
    37 lemmas not_less2not_eq = not_below2not_eq
    38 lemmas less_UU_iff = below_UU_iff
    39 lemmas flat_less_iff = flat_below_iff
    40 lemmas adm_less = adm_below
    41 lemmas adm_not_less = adm_not_below
    42 lemmas adm_compact_not_less = adm_compact_not_below
    43 lemmas less_fun_def = below_fun_def
    44 lemmas expand_fun_less = expand_fun_below
    45 lemmas less_fun_ext = below_fun_ext
    46 lemmas less_discr_def = below_discr_def
    47 lemmas discr_less_eq = discr_below_eq
    48 lemmas less_unit_def = below_unit_def
    49 lemmas less_cprod_def = below_prod_def
    50 lemmas prod_lessI = prod_belowI
    51 lemmas Pair_less_iff = Pair_below_iff
    52 lemmas fst_less_iff = fst_below_iff
    53 lemmas snd_less_iff = snd_below_iff
    54 lemmas expand_cfun_less = expand_cfun_below
    55 lemmas less_cfun_ext = below_cfun_ext
    56 lemmas injection_less = injection_below
    57 lemmas less_up_def = below_up_def
    58 lemmas not_Iup_less = not_Iup_below
    59 lemmas Iup_less = Iup_below
    60 lemmas up_less = up_below
    61 lemmas Def_inject_less_eq = Def_below_Def
    62 lemmas Def_less_is_eq = Def_below_iff
    63 lemmas spair_less_iff = spair_below_iff
    64 lemmas less_sprod = below_sprod
    65 lemmas spair_less = spair_below
    66 lemmas sfst_less_iff = sfst_below_iff
    67 lemmas ssnd_less_iff = ssnd_below_iff
    68 lemmas fix_least_less = fix_least_below
    69 lemmas dist_less_one = dist_below_one
    70 lemmas less_ONE = below_ONE
    71 lemmas ONE_less_iff = ONE_below_iff
    72 lemmas less_sinlD = below_sinlD
    73 lemmas less_sinrD = below_sinrD
    74 
    75 end