src/HOL/IMP/Hoare.ML

 
 open Hoare;
 
 goalw Hoare.thy [hoare_valid_def] "!!P c Q. |- {P}c{Q} ==> |= {P}c{Q}";
 by (etac hoare.induct 1);
-    by(ALLGOALS Asm_simp_tac);
+    by (ALLGOALS Asm_simp_tac);
   by (Fast_tac 1);
  by (Fast_tac 1);
 by (rtac allI 1);
 by (rtac allI 1);
 by (rtac impI 1);
 by (etac induct2 1);
- br Gamma_mono 1;
+ by (rtac Gamma_mono 1);
 by (rewtac Gamma_def);  
 by (Fast_tac 1);
 qed "hoare_sound";
 
 goalw Hoare.thy [swp_def] "swp SKIP Q = Q";
 by (Simp_tac 1);
-by (rtac ext 1);
-by (Fast_tac 1);
 qed "swp_SKIP";
 
 goalw Hoare.thy [swp_def] "swp (x:=a) Q = (%s.Q(s[a s/x]))";
 by (Simp_tac 1);
 qed "swp_Ass";

 qed "swp_While_True";
 
 goalw Hoare.thy [swp_def] "!!s. ~b s ==> swp (WHILE b DO c) Q s = Q s";
 by (stac C_While_If 1);
 by (Asm_simp_tac 1);
-by (Fast_tac 1);
 qed "swp_While_False";
 
 Addsimps [swp_SKIP,swp_Ass,swp_Semi,swp_If,swp_While_True,swp_While_False];
 
 (*Not suitable for rewriting: LOOPS!*)

 by (ALLGOALS Simp_tac);
 by (REPEAT_FIRST Fast_tac);
 by (deepen_tac (!claset addIs [hoare.conseq]) 0 1);
 by (Step_tac 1);
 by (rtac hoare.conseq 1);
-  be thin_rl 1;
+  by (etac thin_rl 1);
   by (Fast_tac 1);
- br hoare.While 1;
- br hoare.conseq 1;
-   be thin_rl 3;
-   br allI 3;
-   br impI 3;
-   ba 3;
+ by (rtac hoare.While 1);
+ by (rtac hoare.conseq 1);
+   by (etac thin_rl 3);
+   by (rtac allI 3);
+   by (rtac impI 3);
+   by (assume_tac 3);
   by (Fast_tac 2);
- by(safe_tac HOL_cs);
- by(rotate_tac ~1 1);
- by(Asm_full_simp_tac 1);
+ by (safe_tac HOL_cs);
+ by (rotate_tac ~1 1);
+ by (Asm_full_simp_tac 1);
 by (rotate_tac ~1 1);
 by (Asm_full_simp_tac 1);
 qed_spec_mp "swp_is_pre";
 
 goal Hoare.thy "!!c. |= {P}c{Q} ==> |- {P}c{Q}";