src/HOLCF/HOLCF.thy
author huffman
Tue Dec 16 09:44:59 2008 -0800 (2008-12-16)
changeset 29130 685c9e05a6ab
parent 28892 435f3718ed9d
child 29138 661a8db7e647
permissions -rw-r--r--
new theory Dsum: cpo of disjoint sum
clasohm@1479
     1
(*  Title:      HOLCF/HOLCF.thy
nipkow@243
     2
    ID:         $Id$
clasohm@1479
     3
    Author:     Franz Regensburger
nipkow@243
     4
wenzelm@16841
     5
HOLCF -- a semantic extension of HOL by the LCF logic.
nipkow@243
     6
*)
nipkow@243
     7
huffman@15650
     8
theory HOLCF
huffman@29130
     9
imports
huffman@29130
    10
  Domain ConvexPD Algebraic Universal Dsum Main
wenzelm@16841
    11
uses
wenzelm@16841
    12
  "holcf_logic.ML"
wenzelm@23152
    13
  "Tools/cont_consts.ML"
wenzelm@23152
    14
  "Tools/domain/domain_library.ML"
wenzelm@23152
    15
  "Tools/domain/domain_syntax.ML"
wenzelm@23152
    16
  "Tools/domain/domain_axioms.ML"
wenzelm@23152
    17
  "Tools/domain/domain_theorems.ML"
wenzelm@23152
    18
  "Tools/domain/domain_extender.ML"
wenzelm@23152
    19
  "Tools/adm_tac.ML"
wenzelm@16841
    20
huffman@15650
    21
begin
huffman@15650
    22
huffman@25904
    23
defaultsort pcpo
huffman@25904
    24
wenzelm@26339
    25
declaration {* fn _ =>
wenzelm@26339
    26
  Simplifier.map_ss (fn simpset => simpset addSolver
wenzelm@17612
    27
    (mk_solver' "adm_tac" (fn ss =>
wenzelm@17876
    28
      adm_tac (cut_facts_tac (Simplifier.prems_of_ss ss) THEN' cont_tacRs ss))));
wenzelm@16841
    29
*}
wenzelm@16841
    30
huffman@15650
    31
end