src/HOLCF/HOLCF.ML
author paulson
Wed, 19 Jul 2006 11:55:26 +0200
changeset 20153 6ff5d35749b0
parent 16841 228d663cc9b3
permissions -rw-r--r--
Fixed the bugs introduced by the last commit! Output is now *identical* to that produced by the old version, based on a-lists.
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$
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     3
*)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     4
15650
b37dc98fbbc5 converted to new-style theory
huffman
parents: 14981
diff changeset
     5
structure HOLCF =
b37dc98fbbc5 converted to new-style theory
huffman
parents: 14981
diff changeset
     6
struct
b37dc98fbbc5 converted to new-style theory
huffman
parents: 14981
diff changeset
     7
  val thy = the_context ();
b37dc98fbbc5 converted to new-style theory
huffman
parents: 14981
diff changeset
     8
end;