1.1 --- a/src/HOL/Hoare/Hoare.ML	Fri Mar 24 21:09:34 2000 +0100
     1.2 +++ b/src/HOL/Hoare/Hoare.ML	Fri Mar 24 21:15:56 2000 +0100
     1.3 @@ -1,4 +1,4 @@
     1.4 -(*  Title:      HOL/Hoare/Hoare.ML
     1.5 +(*  Title:      hoare_vcg.thy
     1.6      ID:         $Id$
     1.7      Author:     Leonor Prensa Nieto & Tobias Nipkow
     1.8      Copyright   1998 TUM
     1.9 @@ -24,7 +24,7 @@
    1.10  Goalw [Valid_def]
    1.11   "[| p <= {s. (s:b --> s:w) & (s~:b --> s:w')}; \
    1.12  \    Valid w c1 q; Valid w' c2 q |] \
    1.13 -\ ==> Valid p (IF b THEN c1 ELSE c2 FI) q";
    1.14 +\ ==> Valid p (Cond b c1 c2) q";
    1.15  by (Asm_simp_tac 1);
    1.16  by (Blast_tac 1);
    1.17  qed "CondRule";
    1.18 @@ -39,7 +39,7 @@
    1.19  
    1.20  Goalw [Valid_def]
    1.21   "[| p <= i; Valid (i Int b) c i;  i Int (-b) <= q |] \
    1.22 -\ ==> Valid p (WHILE b INV {i} DO c OD) q";
    1.23 +\ ==> Valid p (While b i c) q";
    1.24  by (Asm_simp_tac 1);
    1.25  by (Clarify_tac 1);
    1.26  by (dtac lemma 1);
    1.27 @@ -133,7 +133,7 @@
    1.28  (** input does not suffer any unexpected transformation                     **)
    1.29  (*****************************************************************************)
    1.30  
    1.31 -val Compl_Collect = prove_goal thy "-(Collect b) = {x. ~(b x)}"
    1.32 +val Compl_Collect = prove_goal (the_context ()) "-(Collect b) = {x. ~(b x)}"
    1.33      (fn _ => [Fast_tac 1]);
    1.34  
    1.35  (**Simp_tacs**)
    1.36 @@ -208,3 +208,13 @@
    1.37  fun hoare_tac tac i thm =
    1.38    let val Mlem = Mset(thm)
    1.39    in SELECT_GOAL(EVERY[HoareRuleTac Mlem tac true 1]) i thm end;
    1.40 +
    1.41 +
    1.42 +(* proof method setup *)
    1.43 +
    1.44 +val hoare_method =
    1.45 +  Method.METHOD (fn facts => HEADGOAL (Method.insert_tac facts THEN' hoare_tac (K all_tac)));
    1.46 +
    1.47 +val hoare_setup =
    1.48 + [Method.add_methods
    1.49 +  [("hoare", Method.no_args hoare_method, "verification condition generator for Hoare logic")]];