# HG changeset patch
# User wenzelm
# Date 960070144 -7200
# Node ID ea4dc7603f0bfba5682f80671f80c8e09402d038
# Parent  f12d8ea8618bcc4464bb10a37c81c2e23230bf96
removed method;

diff -r f12d8ea8618b -r ea4dc7603f0b src/HOL/Hoare/Hoare.ML
--- a/src/HOL/Hoare/Hoare.ML	Sun Jun 04 00:00:17 2000 +0200
+++ b/src/HOL/Hoare/Hoare.ML	Sun Jun 04 00:09:04 2000 +0200
@@ -216,13 +216,3 @@
 fun hoare_tac tac i thm =
   let val Mlem = Mset(thm)
   in SELECT_GOAL(EVERY[HoareRuleTac Mlem tac true 1]) i thm end;
-
-
-(* proof method setup *)
-
-val hoare_method =
-  Method.METHOD (fn facts => HEADGOAL (Method.insert_tac facts THEN' hoare_tac (K all_tac)));
-
-val hoare_setup =
- [Method.add_methods
-  [("hoare", Method.no_args hoare_method, "verification condition generator for Hoare logic")]];