# HG changeset patch
# User huffman
# Date 1227652166 -3600
# Node ID 435f3718ed9dec20cb52fc8410c120773ba2b5ff
# Parent  f199def7a6a5e79d3c9a23f94d0119f65a8cfb93
add Algebraic and Universal to imports

diff -r f199def7a6a5 -r 435f3718ed9d src/HOLCF/HOLCF.thy
--- a/src/HOLCF/HOLCF.thy	Tue Nov 25 23:29:01 2008 +0100
+++ b/src/HOLCF/HOLCF.thy	Tue Nov 25 23:29:26 2008 +0100
@@ -6,7 +6,7 @@
 *)
 
 theory HOLCF
-imports Sprod Ssum Up Lift Discrete One Tr Domain ConvexPD Main
+imports Sprod Ssum Up Lift Discrete One Tr Domain ConvexPD Algebraic Universal Main
 uses
   "holcf_logic.ML"
   "Tools/cont_consts.ML"