src/HOLCF/HOLCF.thy
author wenzelm
Thu, 14 Jul 2005 19:28:23 +0200
changeset 16841 228d663cc9b3
parent 16054 b8ba6727712f
child 17612 5b37787d2d9e
permissions -rw-r--r--
use all files in HOLCF.thy;
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
15742
64eae3513064 speed improvements for the domain package
huffman
parents: 15651
diff changeset
     9
imports Sprod Ssum Up Lift Discrete One Tr Domain
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"
228d663cc9b3 use all files in HOLCF.thy;
wenzelm
parents: 16054
diff changeset
    12
  "cont_consts.ML"
228d663cc9b3 use all files in HOLCF.thy;
wenzelm
parents: 16054
diff changeset
    13
  "domain/library.ML"
228d663cc9b3 use all files in HOLCF.thy;
wenzelm
parents: 16054
diff changeset
    14
  "domain/syntax.ML"
228d663cc9b3 use all files in HOLCF.thy;
wenzelm
parents: 16054
diff changeset
    15
  "domain/axioms.ML"
228d663cc9b3 use all files in HOLCF.thy;
wenzelm
parents: 16054
diff changeset
    16
  "domain/theorems.ML"
228d663cc9b3 use all files in HOLCF.thy;
wenzelm
parents: 16054
diff changeset
    17
  "domain/extender.ML"
228d663cc9b3 use all files in HOLCF.thy;
wenzelm
parents: 16054
diff changeset
    18
  "domain/interface.ML"
228d663cc9b3 use all files in HOLCF.thy;
wenzelm
parents: 16054
diff changeset
    19
  "adm_tac.ML"
228d663cc9b3 use all files in HOLCF.thy;
wenzelm
parents: 16054
diff changeset
    20
15650
b37dc98fbbc5 converted to new-style theory
huffman
parents: 15576
diff changeset
    21
begin
b37dc98fbbc5 converted to new-style theory
huffman
parents: 15576
diff changeset
    22
16841
228d663cc9b3 use all files in HOLCF.thy;
wenzelm
parents: 16054
diff changeset
    23
ML_setup {*
228d663cc9b3 use all files in HOLCF.thy;
wenzelm
parents: 16054
diff changeset
    24
  simpset_ref() := simpset() addSolver
228d663cc9b3 use all files in HOLCF.thy;
wenzelm
parents: 16054
diff changeset
    25
     (mk_solver "adm_tac" (fn thms => (adm_tac (cut_facts_tac thms THEN' cont_tacRs))));
228d663cc9b3 use all files in HOLCF.thy;
wenzelm
parents: 16054
diff changeset
    26
*}
228d663cc9b3 use all files in HOLCF.thy;
wenzelm
parents: 16054
diff changeset
    27
15650
b37dc98fbbc5 converted to new-style theory
huffman
parents: 15576
diff changeset
    28
end