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
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@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@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@40002
    33
huffman@15650
    34
end