# HG changeset patch
# User kleing
# Date 1036797145 -3600
# Node ID a36a0d417133627322fae3880b2afac811b8d0ca
# Parent  c7cf8fa665341792165206892edb3cdb53af9eb9
Hoare.ML -> hoare.ML

diff -r c7cf8fa66534 -r a36a0d417133 src/HOL/IsaMakefile
--- 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
 
 
diff -r c7cf8fa66534 -r a36a0d417133 src/HOL/Isar_examples/Hoare.thy
--- 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