src/HOL/HOLCF/HOLCF.thy
author huffman
Sat Nov 27 16:08:10 2010 -0800 (2010-11-27)
changeset 40774 0437dbc127b3
parent 40771 src/HOLCF/HOLCF.thy@1c6f7d4b110e
child 41027 c599955d9806
permissions -rw-r--r--
moved directory src/HOLCF to src/HOL/HOLCF;
added HOLCF theories to src/HOL/IsaMakefile;
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
huffman@40497
    14
default_sort "domain"
huffman@25904
    15
huffman@40774
    16
ML {* path_add "~~/src/HOL/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@40011
    26
lemmas monofun_fun_fun = fun_belowD
huffman@40011
    27
lemmas monofun_fun_arg = monofunE
huffman@40011
    28
lemmas monofun_lub_fun = adm_monofun [THEN admD]
huffman@40011
    29
lemmas cont_lub_fun = adm_cont [THEN admD]
huffman@40326
    30
lemmas cont2cont_Rep_CFun = cont2cont_APP
huffman@40326
    31
lemmas cont_Rep_CFun_app = cont_APP_app
huffman@40326
    32
lemmas cont_Rep_CFun_app_app = cont_APP_app_app
huffman@40771
    33
lemmas cont_cfun_fun = cont_Rep_cfun1 [THEN contE]
huffman@40771
    34
lemmas cont_cfun_arg = cont_Rep_cfun2 [THEN contE]
huffman@40771
    35
(*
huffman@40771
    36
lemmas thelubI = lub_eqI
huffman@40771
    37
*)
huffman@40002
    38
huffman@15650
    39
end