src/HOLCF/HOLCF.thy
author paulson
Fri, 05 Oct 2007 09:59:03 +0200
changeset 24854 0ebcd575d3c6
parent 23152 9497234a2743
child 25904 8161f137b0e9
permissions -rw-r--r--
filtering out some package theorems
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"
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
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