src/HOLCF/HOLCF.thy
author huffman
Sun, 19 Feb 2006 02:11:27 +0100
changeset 19105 3aabd46340e0
parent 17923 18c66ca0c776
child 23152 9497234a2743
permissions -rw-r--r--
use minimal 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
19105
3aabd46340e0 use minimal imports
huffman
parents: 17923
diff changeset
     9
imports Sprod Ssum Up Lift Discrete One Tr Domain 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"
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
  "adm_tac.ML"
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
16841
228d663cc9b3 use all files in HOLCF.thy;
wenzelm
parents: 16054
diff changeset
    22
ML_setup {*
17876
b9c92f384109 change_claset/simpset;
wenzelm
parents: 17612
diff changeset
    23
  change_simpset (fn simpset => simpset addSolver
17612
5b37787d2d9e adm_tac/cont_tacRs: proper simpset;
wenzelm
parents: 16841
diff changeset
    24
    (mk_solver' "adm_tac" (fn ss =>
17876
b9c92f384109 change_claset/simpset;
wenzelm
parents: 17612
diff changeset
    25
      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
    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