--- a/src/HOL/Isar_examples/Hoare.thy Wed Aug 29 11:10:59 2007 +0200
+++ b/src/HOL/Isar_examples/Hoare.thy Wed Aug 29 13:58:00 2007 +0200
@@ -8,7 +8,7 @@
header {* Hoare Logic *}
theory Hoare imports Main
-uses ("~~/src/HOL/Hoare/hoare.ML") begin
+uses ("~~/src/HOL/Hoare/hoare_tac.ML") begin
subsection {* Abstract syntax and semantics *}
@@ -442,8 +442,7 @@
apply blast
done
-ML {* val Valid_def = thm "Valid_def" *}
-use "~~/src/HOL/Hoare/hoare.ML"
+use "~~/src/HOL/Hoare/hoare_tac.ML"
method_setup hoare = {*
Method.no_args