--- a/src/HOL/Isar_examples/Hoare.thy Fri Nov 08 10:34:40 2002 +0100
+++ b/src/HOL/Isar_examples/Hoare.thy Sat Nov 09 00:12:25 2002 +0100
@@ -8,7 +8,7 @@
header {* Hoare Logic *}
theory Hoare = Main
-files ("~~/src/HOL/Hoare/Hoare.ML"):
+files ("~~/src/HOL/Hoare/hoare.ML"):
subsection {* Abstract syntax and semantics *}
@@ -411,11 +411,11 @@
*}
ML {* val Valid_def = thm "Valid_def" *}
-use "~~/src/HOL/Hoare/Hoare.ML"
+use "~~/src/HOL/Hoare/hoare.ML"
method_setup hoare = {*
Method.no_args
(Method.SIMPLE_METHOD' HEADGOAL (hoare_tac (K all_tac))) *}
"verification condition generator for Hoare logic"
-end
\ No newline at end of file
+end