# HG changeset patch
# User oheimb
# Date 964025847 -7200
# Node ID c97111953a66a95087ef043658731a5bb422dabb
# Parent  c8e6529cc082e10ad63c0736c32995354c145c51
corrected header

diff -r c8e6529cc082 -r c97111953a66 src/HOL/Hoare/Examples.ML
--- a/src/HOL/Hoare/Examples.ML	Wed Jul 19 12:33:36 2000 +0200
+++ b/src/HOL/Hoare/Examples.ML	Wed Jul 19 18:57:27 2000 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Hoare/Examples.thy
+(*  Title:      HOL/Hoare/Examples.ML
     ID:         $Id$
     Author:     Norbert Galm & Tobias Nipkow
     Copyright   1998 TUM
diff -r c8e6529cc082 -r c97111953a66 src/HOL/Hoare/Hoare.ML
--- a/src/HOL/Hoare/Hoare.ML	Wed Jul 19 12:33:36 2000 +0200
+++ b/src/HOL/Hoare/Hoare.ML	Wed Jul 19 18:57:27 2000 +0200
@@ -1,4 +1,4 @@
-(*  Title:      hoare_vcg.thy
+(*  Title:      HOL/Hoare/Hoare.ML
     ID:         $Id$
     Author:     Leonor Prensa Nieto & Tobias Nipkow
     Copyright   1998 TUM