--- a/src/HOL/Isar_examples/Hoare.thy Mon Jun 22 22:51:08 2009 +0200
+++ b/src/HOL/Isar_examples/Hoare.thy Mon Jun 22 23:48:24 2009 +0200
@@ -1,5 +1,4 @@
(* Title: HOL/Isar_examples/Hoare.thy
- ID: $Id$
Author: Markus Wenzel, TU Muenchen
A formulation of Hoare logic suitable for Isar.
@@ -7,8 +6,10 @@
header {* Hoare Logic *}
-theory Hoare imports Main
-uses ("~~/src/HOL/Hoare/hoare_tac.ML") begin
+theory Hoare
+imports Main
+uses ("~~/src/HOL/Hoare/hoare_tac.ML")
+begin
subsection {* Abstract syntax and semantics *}