src/HOL/IMP/Hoare.ML

--- a/src/HOL/IMP/Hoare.ML	Mon Jun 22 17:13:09 1998 +0200
+++ b/src/HOL/IMP/Hoare.ML	Mon Jun 22 17:26:46 1998 +0200
@@ -9,7 +9,7 @@
 
 open Hoare;
 
-goalw Hoare.thy [hoare_valid_def] "!!P c Q. |- {P}c{Q} ==> |= {P}c{Q}";
+Goalw [hoare_valid_def] "!!P c Q. |- {P}c{Q} ==> |= {P}c{Q}";
 by (etac hoare.induct 1);
     by (ALLGOALS Asm_simp_tac);
   by (Fast_tac 1);
@@ -23,21 +23,21 @@
 by (Fast_tac 1);
 qed "hoare_sound";
 
-goalw Hoare.thy [wp_def] "wp SKIP Q = Q";
+Goalw [wp_def] "wp SKIP Q = Q";
 by (Simp_tac 1);
 qed "wp_SKIP";
 
-goalw Hoare.thy [wp_def] "wp (x:=a) Q = (%s. Q(s[x:=a s]))";
+Goalw [wp_def] "wp (x:=a) Q = (%s. Q(s[x:=a s]))";
 by (Simp_tac 1);
 qed "wp_Ass";
 
-goalw Hoare.thy [wp_def] "wp (c;d) Q = wp c (wp d Q)";
+Goalw [wp_def] "wp (c;d) Q = wp c (wp d Q)";
 by (Simp_tac 1);
 by (rtac ext 1);
 by (Fast_tac 1);
 qed "wp_Semi";
 
-goalw Hoare.thy [wp_def]
+Goalw [wp_def]
   "wp (IF b THEN c ELSE d) Q = (%s. (b s --> wp c Q s) & \
 \                                    (~b s --> wp d Q s))";
 by (Simp_tac 1);
@@ -45,13 +45,13 @@
 by (Fast_tac 1);
 qed "wp_If";
 
-goalw Hoare.thy [wp_def]
+Goalw [wp_def]
   "!!s. b s ==> wp (WHILE b DO c) Q s = wp (c;WHILE b DO c) Q s";
 by (stac C_While_If 1);
 by (Asm_simp_tac 1);
 qed "wp_While_True";
 
-goalw Hoare.thy [wp_def] "!!s. ~b s ==> wp (WHILE b DO c) Q s = Q s";
+Goalw [wp_def] "!!s. ~b s ==> wp (WHILE b DO c) Q s = Q s";
 by (stac C_While_If 1);
 by (Asm_simp_tac 1);
 qed "wp_While_False";
@@ -59,12 +59,12 @@
 Addsimps [wp_SKIP,wp_Ass,wp_Semi,wp_If,wp_While_True,wp_While_False];
 
 (*Not suitable for rewriting: LOOPS!*)
-goal Hoare.thy "wp (WHILE b DO c) Q s = \
+Goal "wp (WHILE b DO c) Q s = \
 \                 (if b s then wp (c;WHILE b DO c) Q s else Q s)";
 by (Simp_tac 1);
 qed "wp_While_if";
 
-goal thy
+Goal
   "wp (WHILE b DO c) Q s = \
 \  (s : gfp(%S.{s. if b s then wp c (%s. s:S) s else Q s}))";
 by (Simp_tac 1);
@@ -91,7 +91,7 @@
 
 AddSIs [hoare.skip, hoare.ass, hoare.semi, hoare.If];
 
-goal Hoare.thy "!Q. |- {wp c Q} c {Q}";
+Goal "!Q. |- {wp c Q} c {Q}";
 by (com.induct_tac "c" 1);
 by (ALLGOALS Simp_tac);
 by (REPEAT_FIRST Fast_tac);
@@ -114,7 +114,7 @@
 by (Asm_full_simp_tac 1);
 qed_spec_mp "wp_is_pre";
 
-goal Hoare.thy "!!c. |= {P}c{Q} ==> |- {P}c{Q}";
+Goal "!!c. |= {P}c{Q} ==> |- {P}c{Q}";
 by (rtac (wp_is_pre RSN (2,hoare.conseq)) 1);
  by (Fast_tac 2);
 by (rewrite_goals_tac [hoare_valid_def,wp_def]);