src/HOLCF/HOLCF.thy
author wenzelm
Fri Mar 20 11:26:25 2009 +0100 (2009-03-20)
changeset 30603 71180005f251
parent 29542 d20f453eb4a3
child 30910 a7cc0ef93269
permissions -rw-r--r--
proper context for prove_cont/adm_tac;
clasohm@1479
     1
(*  Title:      HOLCF/HOLCF.thy
clasohm@1479
     2
    Author:     Franz Regensburger
nipkow@243
     3
wenzelm@16841
     4
HOLCF -- a semantic extension of HOL by the LCF logic.
nipkow@243
     5
*)
nipkow@243
     6
huffman@15650
     7
theory HOLCF
huffman@29130
     8
imports
huffman@29534
     9
  Domain ConvexPD Algebraic Universal Sum_Cpo Main
wenzelm@16841
    10
uses
wenzelm@16841
    11
  "holcf_logic.ML"
wenzelm@23152
    12
  "Tools/cont_consts.ML"
huffman@29530
    13
  "Tools/cont_proc.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"
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@30603
    27
      Adm.adm_tac (Simplifier.the_context ss)
wenzelm@30603
    28
        (cut_facts_tac (Simplifier.prems_of_ss ss) THEN' cont_tacRs ss))));
wenzelm@16841
    29
*}
wenzelm@16841
    30
huffman@15650
    31
end