src/HOLCF/HOLCF.ML
author huffman
Sat, 04 Jun 2005 00:22:08 +0200
changeset 16221 879400e029bf
parent 16062 f8110bd9957f
child 16841 228d663cc9b3
permissions -rw-r--r--
New theory with lemmas for the fixrec package
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1274
diff changeset
     1
(*  Title:      HOLCF/HOLCF.ML
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     2
    ID:         $Id$
1461
6bcb44e4d6e5 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
*)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     5
15650
b37dc98fbbc5 converted to new-style theory
huffman
parents: 14981
diff changeset
     6
structure HOLCF =
b37dc98fbbc5 converted to new-style theory
huffman
parents: 14981
diff changeset
     7
struct
b37dc98fbbc5 converted to new-style theory
huffman
parents: 14981
diff changeset
     8
  val thy = the_context ();
b37dc98fbbc5 converted to new-style theory
huffman
parents: 14981
diff changeset
     9
end;
b37dc98fbbc5 converted to new-style theory
huffman
parents: 14981
diff changeset
    10
16062
f8110bd9957f cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents: 15650
diff changeset
    11
use "adm_tac.ML";
3661
1ea4a45b9412 moved extended adm_tac to new place
mueller
parents: 2355
diff changeset
    12
7570
a9391550eea1 Mod because of new solver interface.
nipkow
parents: 4098
diff changeset
    13
simpset_ref() := simpset() addSolver
a9391550eea1 Mod because of new solver interface.
nipkow
parents: 4098
diff changeset
    14
   (mk_solver "adm_tac" (fn thms => (adm_tac (cut_facts_tac thms THEN' cont_tacRs))));
3661
1ea4a45b9412 moved extended adm_tac to new place
mueller
parents: 2355
diff changeset
    15
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3661
diff changeset
    16
val HOLCF_ss = simpset();