author | nipkow |
Fri, 17 May 1996 12:24:47 +0200 | |
changeset 1747 | f20c9abe4b50 |
parent 1746 | f0c6aabc6c02 |
child 1748 | 88650ba93c10 |
--- a/src/HOL/IMP/Hoare.ML Fri May 17 12:23:44 1996 +0200 +++ b/src/HOL/IMP/Hoare.ML Fri May 17 12:24:47 1996 +0200 @@ -19,8 +19,10 @@ 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","a")] allE 1); +by(eres_inst_tac [("x","s")] allE 1); by (safe_tac comp_cs); by(ALLGOALS Asm_full_simp_tac); qed "hoare_sound";