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