--- a/src/HOL/IMP/Hoare.ML Tue Sep 10 11:37:52 1996 +0200
+++ b/src/HOL/IMP/Hoare.ML Tue Sep 10 20:10:29 1996 +0200
@@ -12,19 +12,15 @@
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(fast_tac rel_cs 1);
+ 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(prune_params_tac);
-by(rename_tac "s t" 1);
by (rewtac Gamma_def);
-by(eres_inst_tac [("x","s")] allE 1);
-by (Step_tac 1);
- by(ALLGOALS Asm_full_simp_tac);
+by (Fast_tac 1);
qed "hoare_sound";
goalw Hoare.thy [swp_def] "swp SKIP Q = Q";