# HG changeset patch
# User huffman
# Date 1112393558 -7200
# Node ID b37dc98fbbc536d08345fdcd3c43d02c7667286c
# Parent  f8345ee4f60759a9d77628084af6775a78dafdd6
converted to new-style theory

diff -r f8345ee4f607 -r b37dc98fbbc5 src/HOLCF/HOLCF.ML
--- a/src/HOLCF/HOLCF.ML	Fri Apr 01 23:44:41 2005 +0200
+++ b/src/HOLCF/HOLCF.ML	Sat Apr 02 00:12:38 2005 +0200
@@ -3,6 +3,11 @@
     Author:     Franz Regensburger
 *)
 
+structure HOLCF =
+struct
+  val thy = the_context ();
+end;
+
 use"adm.ML";
 
 simpset_ref() := simpset() addSolver
diff -r f8345ee4f607 -r b37dc98fbbc5 src/HOLCF/HOLCF.thy
--- a/src/HOLCF/HOLCF.thy	Fri Apr 01 23:44:41 2005 +0200
+++ b/src/HOLCF/HOLCF.thy	Sat Apr 02 00:12:38 2005 +0200
@@ -5,4 +5,8 @@
 Top theory for HOLCF system.
 *)
 
-HOLCF = Sprod + Ssum + Up + Lift + Discrete + One + Tr
+theory HOLCF
+imports Sprod Ssum Up Lift Discrete One Tr
+begin
+
+end