src/HOLCF/HOLCF.thy
author huffman
Tue, 25 Nov 2008 23:29:26 +0100
changeset 28892 435f3718ed9d
parent 26339 7825c83c9eff
child 29130 685c9e05a6ab
permissions -rw-r--r--
add Algebraic and Universal to imports
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1479
21eb5e156d91 expanded tabs
clasohm
parents: 1274
diff changeset
     1
(*  Title:      HOLCF/HOLCF.thy
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     2
    ID:         $Id$
1479
21eb5e156d91 expanded tabs
clasohm
parents: 1274
diff changeset
     3
    Author:     Franz Regensburger
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     4
16841
228d663cc9b3 use all files in HOLCF.thy;
wenzelm
parents: 16054
diff changeset
     5
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
     6
*)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     7
15650
b37dc98fbbc5 converted to new-style theory
huffman
parents: 15576
diff changeset
     8
theory HOLCF
28892
435f3718ed9d add Algebraic and Universal to imports
huffman
parents: 26339
diff changeset
     9
imports Sprod Ssum Up Lift Discrete One Tr Domain ConvexPD Algebraic Universal Main
16841
228d663cc9b3 use all files in HOLCF.thy;
wenzelm
parents: 16054
diff changeset
    10
uses
228d663cc9b3 use all files in HOLCF.thy;
wenzelm
parents: 16054
diff changeset
    11
  "holcf_logic.ML"
23152
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents: 19105
diff changeset
    12
  "Tools/cont_consts.ML"
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents: 19105
diff changeset
    13
  "Tools/domain/domain_library.ML"
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents: 19105
diff changeset
    14
  "Tools/domain/domain_syntax.ML"
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents: 19105
diff changeset
    15
  "Tools/domain/domain_axioms.ML"
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents: 19105
diff changeset
    16
  "Tools/domain/domain_theorems.ML"
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents: 19105
diff changeset
    17
  "Tools/domain/domain_extender.ML"
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents: 19105
diff changeset
    18
  "Tools/adm_tac.ML"
16841
228d663cc9b3 use all files in HOLCF.thy;
wenzelm
parents: 16054
diff changeset
    19
15650
b37dc98fbbc5 converted to new-style theory
huffman
parents: 15576
diff changeset
    20
begin
b37dc98fbbc5 converted to new-style theory
huffman
parents: 15576
diff changeset
    21
25904
8161f137b0e9 new theory of powerdomains
huffman
parents: 23152
diff changeset
    22
defaultsort pcpo
8161f137b0e9 new theory of powerdomains
huffman
parents: 23152
diff changeset
    23
26339
7825c83c9eff eliminated change_claset/simpset;
wenzelm
parents: 25904
diff changeset
    24
declaration {* fn _ =>
7825c83c9eff eliminated change_claset/simpset;
wenzelm
parents: 25904
diff changeset
    25
  Simplifier.map_ss (fn simpset => simpset addSolver
17612
5b37787d2d9e adm_tac/cont_tacRs: proper simpset;
wenzelm
parents: 16841
diff changeset
    26
    (mk_solver' "adm_tac" (fn ss =>
17876
b9c92f384109 change_claset/simpset;
wenzelm
parents: 17612
diff changeset
    27
      adm_tac (cut_facts_tac (Simplifier.prems_of_ss ss) THEN' cont_tacRs ss))));
16841
228d663cc9b3 use all files in HOLCF.thy;
wenzelm
parents: 16054
diff changeset
    28
*}
228d663cc9b3 use all files in HOLCF.thy;
wenzelm
parents: 16054
diff changeset
    29
15650
b37dc98fbbc5 converted to new-style theory
huffman
parents: 15576
diff changeset
    30
end