src/HOLCF/HOLCF.thy
author huffman
Wed, 03 Nov 2010 15:47:46 -0700
changeset 40431 682d6c455670
parent 40329 73f2b99b549d
child 40497 d2e876d6da8c
permissions -rw-r--r--
discontinue a bunch of legacy theorem names
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1479
21eb5e156d91 expanded tabs
clasohm
parents: 1274
diff changeset
     1
(*  Title:      HOLCF/HOLCF.thy
21eb5e156d91 expanded tabs
clasohm
parents: 1274
diff changeset
     2
    Author:     Franz Regensburger
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     3
16841
228d663cc9b3 use all files in HOLCF.thy;
wenzelm
parents: 16054
diff changeset
     4
HOLCF -- a semantic extension of HOL by the LCF logic.
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     5
*)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     6
15650
b37dc98fbbc5 converted to new-style theory
huffman
parents: 15576
diff changeset
     7
theory HOLCF
29130
685c9e05a6ab new theory Dsum: cpo of disjoint sum
huffman
parents: 28892
diff changeset
     8
imports
35473
c4d3d65856dd move some powerdomain stuff into a new file
huffman
parents: 33588
diff changeset
     9
  Main
c4d3d65856dd move some powerdomain stuff into a new file
huffman
parents: 33588
diff changeset
    10
  Domain
c4d3d65856dd move some powerdomain stuff into a new file
huffman
parents: 33588
diff changeset
    11
  Powerdomains
15650
b37dc98fbbc5 converted to new-style theory
huffman
parents: 15576
diff changeset
    12
begin
b37dc98fbbc5 converted to new-style theory
huffman
parents: 15576
diff changeset
    13
40329
73f2b99b549d change default_sort of HOLCF from pcpo to bifinite; rename command 'new_domain' to 'domain'; rename 'domain' to 'domain (unsafe)'
huffman
parents: 40326
diff changeset
    14
default_sort bifinite
25904
8161f137b0e9 new theory of powerdomains
huffman
parents: 23152
diff changeset
    15
37110
7ffdbc24b27f move Strict_Fun and Stream theories to new HOLCF/Library directory; add HOLCF/Library to search path
huffman
parents: 36452
diff changeset
    16
ML {* path_add "~~/src/HOLCF/Library" *}
7ffdbc24b27f move Strict_Fun and Stream theories to new HOLCF/Library directory; add HOLCF/Library to search path
huffman
parents: 36452
diff changeset
    17
40002
c5b5f7a3a3b1 new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI
huffman
parents: 39974
diff changeset
    18
text {* Legacy theorem names deprecated after Isabelle2009-2: *}
c5b5f7a3a3b1 new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI
huffman
parents: 39974
diff changeset
    19
c5b5f7a3a3b1 new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI
huffman
parents: 39974
diff changeset
    20
lemmas expand_fun_below = fun_below_iff
c5b5f7a3a3b1 new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI
huffman
parents: 39974
diff changeset
    21
lemmas below_fun_ext = fun_belowI
c5b5f7a3a3b1 new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI
huffman
parents: 39974
diff changeset
    22
lemmas expand_cfun_eq = cfun_eq_iff
c5b5f7a3a3b1 new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI
huffman
parents: 39974
diff changeset
    23
lemmas ext_cfun = cfun_eqI
c5b5f7a3a3b1 new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI
huffman
parents: 39974
diff changeset
    24
lemmas expand_cfun_below = cfun_below_iff
c5b5f7a3a3b1 new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI
huffman
parents: 39974
diff changeset
    25
lemmas below_cfun_ext = cfun_belowI
40011
b974cf829099 cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents: 40002
diff changeset
    26
lemmas monofun_fun_fun = fun_belowD
b974cf829099 cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents: 40002
diff changeset
    27
lemmas monofun_fun_arg = monofunE
b974cf829099 cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents: 40002
diff changeset
    28
lemmas monofun_lub_fun = adm_monofun [THEN admD]
b974cf829099 cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents: 40002
diff changeset
    29
lemmas cont_lub_fun = adm_cont [THEN admD]
40326
73d45866dbda renamed lemma cont2cont_Rep_CFun to cont2cont_APP
huffman
parents: 40011
diff changeset
    30
lemmas cont2cont_Rep_CFun = cont2cont_APP
73d45866dbda renamed lemma cont2cont_Rep_CFun to cont2cont_APP
huffman
parents: 40011
diff changeset
    31
lemmas cont_Rep_CFun_app = cont_APP_app
73d45866dbda renamed lemma cont2cont_Rep_CFun to cont2cont_APP
huffman
parents: 40011
diff changeset
    32
lemmas cont_Rep_CFun_app_app = cont_APP_app_app
40002
c5b5f7a3a3b1 new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI
huffman
parents: 39974
diff changeset
    33
15650
b37dc98fbbc5 converted to new-style theory
huffman
parents: 15576
diff changeset
    34
end