# HG changeset patch
# User oheimb
# Date 962981276 -7200
# Node ID 9e619ac0fe2f251c35817a7df1f76622e6e01bfc
# Parent  5f39d82606aad5c096d6c51049d96c9ea103911c
added dependency caveat

diff -r 5f39d82606aa -r 9e619ac0fe2f src/HOL/IMP/ROOT.ML
--- a/src/HOL/IMP/ROOT.ML	Fri Jul 07 16:46:02 2000 +0200
+++ b/src/HOL/IMP/ROOT.ML	Fri Jul 07 16:47:56 2000 +0200
@@ -2,6 +2,8 @@
     ID:         $Id$
     Author:     Heiko Loetzbeyer, Robert Sandner, Tobias Nipkow
     Copyright   1995 TUM
+
+Caveat: HOLCF/IMP depends on HOL/IMP
 *)
 
 time_use_thy "Expr";