# HG changeset patch
# User oheimb
# Date 962981292 -7200
# Node ID a0a7c31cdc398a2dcfe155fdabb3d8c2ac517627
# Parent  9e619ac0fe2f251c35817a7df1f76622e6e01bfc
added dependency caveat

diff -r 9e619ac0fe2f -r a0a7c31cdc39 src/HOL/IMP/ROOT.ML
--- a/src/HOL/IMP/ROOT.ML	Fri Jul 07 16:47:56 2000 +0200
+++ b/src/HOL/IMP/ROOT.ML	Fri Jul 07 16:48:12 2000 +0200
@@ -1,7 +1,7 @@
-(*  Title:      HOL/IMP/ROOT.ML
-    ID:         $Id$
-    Author:     Heiko Loetzbeyer, Robert Sandner, Tobias Nipkow
-    Copyright   1995 TUM
+(*  Title:     HOL/IMP/ROOT.ML
+    ID:        $Id$
+    Author:    Heiko Loetzbeyer, Robert Sandner, Tobias Nipkow, David von Oheimb
+    Copyright  1995 TUM
 
 Caveat: HOLCF/IMP depends on HOL/IMP
 *)