# HG changeset patch
# User wenzelm
# Date 976561842 -3600
# Node ID 5be46cd1f94a28032ff7de1a48195aa0ed528573
# Parent  d1533f63c73814d414865169952232d91b7c125c
tuned;

diff -r d1533f63c738 -r 5be46cd1f94a src/HOL/Hoare/Hoare.ML
--- 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);