| 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-- |
| 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 |