src/HOL/IMP/ROOT.ML
changeset 9277 a0a7c31cdc39
parent 9276 9e619ac0fe2f
child 10342 b124d59f7b61
     1.1 --- a/src/HOL/IMP/ROOT.ML	Fri Jul 07 16:47:56 2000 +0200
     1.2 +++ b/src/HOL/IMP/ROOT.ML	Fri Jul 07 16:48:12 2000 +0200
     1.3 @@ -1,7 +1,7 @@
     1.4 -(*  Title:      HOL/IMP/ROOT.ML
     1.5 -    ID:         $Id$
     1.6 -    Author:     Heiko Loetzbeyer, Robert Sandner, Tobias Nipkow
     1.7 -    Copyright   1995 TUM
     1.8 +(*  Title:     HOL/IMP/ROOT.ML
     1.9 +    ID:        $Id$
    1.10 +    Author:    Heiko Loetzbeyer, Robert Sandner, Tobias Nipkow, David von Oheimb
    1.11 +    Copyright  1995 TUM
    1.12  
    1.13  Caveat: HOLCF/IMP depends on HOL/IMP
    1.14  *)