src/HOLCF/HOLCF.thy
author wenzelm
Wed Mar 19 22:47:35 2008 +0100 (2008-03-19)
changeset 26339 7825c83c9eff
parent 25904 8161f137b0e9
child 28892 435f3718ed9d
permissions -rw-r--r--
eliminated change_claset/simpset;
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@25904
     9
imports Sprod Ssum Up Lift Discrete One Tr Domain ConvexPD Main
wenzelm@16841
    10
uses
wenzelm@16841
    11
  "holcf_logic.ML"
wenzelm@23152
    12
  "Tools/cont_consts.ML"
wenzelm@23152
    13
  "Tools/domain/domain_library.ML"
wenzelm@23152
    14
  "Tools/domain/domain_syntax.ML"
wenzelm@23152
    15
  "Tools/domain/domain_axioms.ML"
wenzelm@23152
    16
  "Tools/domain/domain_theorems.ML"
wenzelm@23152
    17
  "Tools/domain/domain_extender.ML"
wenzelm@23152
    18
  "Tools/adm_tac.ML"
wenzelm@16841
    19
huffman@15650
    20
begin
huffman@15650
    21
huffman@25904
    22
defaultsort pcpo
huffman@25904
    23
wenzelm@26339
    24
declaration {* fn _ =>
wenzelm@26339
    25
  Simplifier.map_ss (fn simpset => simpset addSolver
wenzelm@17612
    26
    (mk_solver' "adm_tac" (fn ss =>
wenzelm@17876
    27
      adm_tac (cut_facts_tac (Simplifier.prems_of_ss ss) THEN' cont_tacRs ss))));
wenzelm@16841
    28
*}
wenzelm@16841
    29
huffman@15650
    30
end