--- a/src/HOL/Hoare/Hoare.ML Mon Dec 11 20:10:18 2000 +0100
+++ b/src/HOL/Hoare/Hoare.ML Mon Dec 11 20:10:42 2000 +0100
@@ -8,20 +8,20 @@
(*** The proof rules ***)
-Goalw [Valid_def] "p <= q ==> Valid p SKIP q";
+Goalw [thm "Valid_def"] "p <= q ==> Valid p (Basic id) q";
by (Auto_tac);
qed "SkipRule";
-Goalw [Valid_def] "p <= {s. (f s):q} ==> Valid p (Basic f) q";
+Goalw [thm "Valid_def"] "p <= {s. (f s):q} ==> Valid p (Basic f) q";
by (Auto_tac);
qed "BasicRule";
-Goalw [Valid_def] "Valid P c1 Q ==> Valid Q c2 R ==> Valid P (c1;c2) R";
+Goalw [thm "Valid_def"] "Valid P c1 Q ==> Valid Q c2 R ==> Valid P (c1;c2) R";
by (Asm_simp_tac 1);
by (Blast_tac 1);
qed "SeqRule";
-Goalw [Valid_def]
+Goalw [thm "Valid_def"]
"p <= {s. (s:b --> s:w) & (s~:b --> s:w')} \
\ ==> Valid w c1 q ==> Valid w' c2 q \
\ ==> Valid p (Cond b c1 c2) q";
@@ -37,7 +37,7 @@
by (Blast_tac 1);
val lemma = result() RS spec RS spec RS mp RS mp;
-Goalw [Valid_def]
+Goalw [thm "Valid_def"]
"p <= i ==> Valid (i Int b) c i ==> i Int (-b) <= q \
\ ==> Valid p (While b j c) q";
by (Asm_simp_tac 1);