src/HOL/IMP/Hoare.ML

 by (etac hoare.induct 1);
      by (ALLGOALS Asm_simp_tac);
   by (Fast_tac 1);
  by (Fast_tac 1);
 by (EVERY' [rtac allI, rtac allI, rtac impI] 1);
-by (etac induct2 1);
+by (etac lfp_induct2 1);
  by (rtac Gamma_mono 1);
 by (rewtac Gamma_def);  
 by (Fast_tac 1);
 qed "hoare_sound";
 

  by (Asm_full_simp_tac 1);
 by (asm_full_simp_tac (simpset() addsimps [wp_def,Gamma_def]) 1);
 by (strip_tac 1);
 by (rtac mp 1);
  by (assume_tac 2);
-by (etac induct2 1);
+by (etac lfp_induct2 1);
 by (fast_tac (claset() addSIs [monoI]) 1);
 by (stac gfp_unfold 1);
  by (fast_tac (claset() addSIs [monoI]) 1);
 by (Fast_tac 1);
 qed "wp_While";