# HG changeset patch
# User nipkow
# Date 873799708 -7200
# Node ID e2d1e1151314b81d336bfdee83a98259bd57f0ec
# Parent  4be700757406a66fafc178e9f41755253a1dd939
Loads HoareEx now.

diff -r 4be700757406 -r e2d1e1151314 src/HOLCF/IMP/ROOT.ML
--- a/src/HOLCF/IMP/ROOT.ML	Tue Sep 09 11:15:32 1997 +0200
+++ b/src/HOLCF/IMP/ROOT.ML	Tue Sep 09 12:08:28 1997 +0200
@@ -15,4 +15,4 @@
 make_html := old_make_html;
 loadpath := ["."];
 
-use_thy "Denotational";
+use_thy "HoareEx";