--- a/src/HOL/IsaMakefile Fri Nov 08 10:34:40 2002 +0100
+++ b/src/HOL/IsaMakefile Sat Nov 09 00:12:25 2002 +0100
@@ -627,7 +627,7 @@
Isar_examples/Puzzle.thy Isar_examples/Summation.thy \
Isar_examples/ROOT.ML Isar_examples/document/proof.sty \
Isar_examples/document/root.bib Isar_examples/document/root.tex \
- Isar_examples/document/style.tex Hoare/Hoare.ML
+ Isar_examples/document/style.tex Hoare/hoare.ML
@$(ISATOOL) usedir $(OUT)/HOL Isar_examples
--- 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