src/HOLCF/HOLCF.ML
author huffman
Sat Apr 02 00:12:38 2005 +0200 (2005-04-02)
changeset 15650 b37dc98fbbc5
parent 14981 e73f8140af78
child 16062 f8110bd9957f
permissions -rw-r--r--
converted to new-style theory
clasohm@1461
     1
(*  Title:      HOLCF/HOLCF.ML
nipkow@243
     2
    ID:         $Id$
clasohm@1461
     3
    Author:     Franz Regensburger
nipkow@243
     4
*)
nipkow@243
     5
huffman@15650
     6
structure HOLCF =
huffman@15650
     7
struct
huffman@15650
     8
  val thy = the_context ();
huffman@15650
     9
end;
huffman@15650
    10
mueller@3661
    11
use"adm.ML";
mueller@3661
    12
nipkow@7570
    13
simpset_ref() := simpset() addSolver
nipkow@7570
    14
   (mk_solver "adm_tac" (fn thms => (adm_tac (cut_facts_tac thms THEN' cont_tacRs))));
mueller@3661
    15
wenzelm@4098
    16
val HOLCF_ss = simpset();