src/HOL/IMP/ROOT.ML
changeset 9276 9e619ac0fe2f
parent 9241 f961c1fdff50
child 9277 a0a7c31cdc39
     1.1 --- a/src/HOL/IMP/ROOT.ML	Fri Jul 07 16:46:02 2000 +0200
     1.2 +++ b/src/HOL/IMP/ROOT.ML	Fri Jul 07 16:47:56 2000 +0200
     1.3 @@ -2,6 +2,8 @@
     1.4      ID:         $Id$
     1.5      Author:     Heiko Loetzbeyer, Robert Sandner, Tobias Nipkow
     1.6      Copyright   1995 TUM
     1.7 +
     1.8 +Caveat: HOLCF/IMP depends on HOL/IMP
     1.9  *)
    1.10  
    1.11  time_use_thy "Expr";