src/HOLCF/HOLCF.thy
author huffman
Wed Nov 10 17:56:08 2010 -0800 (2010-11-10)
changeset 40502 8e92772bc0e8
parent 40497 d2e876d6da8c
child 40771 1c6f7d4b110e
permissions -rw-r--r--
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
     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 "domain"
    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 lemmas monofun_fun_fun = fun_belowD
    27 lemmas monofun_fun_arg = monofunE
    28 lemmas monofun_lub_fun = adm_monofun [THEN admD]
    29 lemmas cont_lub_fun = adm_cont [THEN admD]
    30 lemmas cont2cont_Rep_CFun = cont2cont_APP
    31 lemmas cont_Rep_CFun_app = cont_APP_app
    32 lemmas cont_Rep_CFun_app_app = cont_APP_app_app
    33 
    34 end