src/HOL/MiniML/W.ML

 by (assume_tac 1);
 qed "new_tv_compatible_W";
 
 goal thy "!!sch. new_tv n sch --> new_tv (n + (min_new_bound_tv sch)) (bound_typ_inst (%b. TVar (b + n)) sch)";
 by (type_scheme.induct_tac "sch" 1);
-by (Asm_full_simp_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [add_commute]) 1);
+  by (Asm_full_simp_tac 1);
+ by (asm_full_simp_tac (simpset() addsimps [add_commute]) 1);
 by (strip_tac 1);
 by (Asm_full_simp_tac 1);
 by (etac conjE 1);
 by (rtac conjI 1);
+ by (rtac new_tv_le 1);
+  by (assume_tac 2);
+ by (rtac add_le_mono 1);
+  by (Simp_tac 1);
+ by (simp_tac (simpset() addsimps [max_def]) 1);
 by (rtac new_tv_le 1);
-by (mp_tac 2);
-by (mp_tac 2);
-by (assume_tac 2);
+ by (assume_tac 2);
 by (rtac add_le_mono 1);
-by (Simp_tac 1);
-by (simp_tac (simpset() addsimps [max_def]) 1);
-by (strip_tac 1);
-by (rtac new_tv_le 1);
-by (mp_tac 2);
-by (mp_tac 2);
-by (assume_tac 2);
-by (rtac add_le_mono 1);
-by (Simp_tac 1);
+ by (Simp_tac 1);
 by (simp_tac (simpset() addsimps [max_def]) 1);
 by (strip_tac 1);
 by (dtac not_leE 1);
 by (rtac less_or_eq_imp_le 1);
 by (Fast_tac 1);

 (** LEVEL 26 **)
 by (eres_inst_tac [("x","R")] allE 1);
 by (eres_inst_tac [("x","$ S A")] allE 1);
 by (eres_inst_tac [("x","t2")] allE 1);
 by (eres_inst_tac [("x","m")] allE 1);
-by (rotate_tac ~3 1);
 by (Asm_full_simp_tac 1);
 by (safe_tac HOL_cs);
-by (contr_tac 1);
 by (fast_tac (HOL_cs addIs [sym RS W_var_geD,new_tv_W RS
         conjunct1,new_scheme_list_le,new_tv_subst_scheme_list]) 1);
 (** LEVEL 35 **)
 by (subgoal_tac
   "$ (%x. if x=ma then t' else (if x:(free_tv t - free_tv Sa) then R x \

 by (Asm_simp_tac 1); 
 by (eres_inst_tac [("x","R")] allE 1);
 by (eres_inst_tac [("x","gen ($ S A) t # $ S A")] allE 1);
 by (eres_inst_tac [("x","t'")] allE 1);
 by (eres_inst_tac [("x","m")] allE 1);
-by (rotate_tac 4 1);
 by (Asm_full_simp_tac 1);
 by (dtac mp 1);
 by (rtac has_type_le_env 1);
 by (assume_tac 1);
 by (Simp_tac 1);