src/HOL/MiniML/W.ML

 by (mp_tac 1);
 by (assume_tac 1);
 (* case Let e1 e2 *)
 by (simp_tac (simpset() addsplits [split_option_bind]) 1);
 by (strip_tac 1);
-by (rename_tac "w q m1 S1 t1 m2 S2 t n2" 1); 
+(*by (rename_tac "w q m1 S1 t1 m2 S2 t n2" 1); *)
+by (rename_tac "S1 t1 m1 S2" 1); 
 by (res_inst_tac [("t1.0","$ S2 t1")] has_type.LETI 1);
-by (simp_tac (simpset() addsimps [o_def]) 1);
-by (simp_tac (HOL_ss addsimps [subst_comp_scheme_list RS sym]) 1);
-by (rtac (has_type_cl_sub RS spec) 1);
-by (dres_inst_tac [("x","A")] spec 1);
-by (dres_inst_tac [("x","S1")] spec 1);
-by (dres_inst_tac [("x","t1")] spec 1);
-by (dres_inst_tac [("x","m2")] spec 1);
-by (rotate_tac 4 1);
-by (dres_inst_tac [("x","m1")] spec 1);
-by (mp_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [eq_sym_conv]) 1);
+ by (simp_tac (simpset() addsimps [o_def]) 1);
+ by (simp_tac (HOL_ss addsimps [subst_comp_scheme_list RS sym]) 1);
+ by (rtac (has_type_cl_sub RS spec) 1);
+ by (dres_inst_tac [("x","A")] spec 1);
+ by (dres_inst_tac [("x","S1")] spec 1);
+ by (dres_inst_tac [("x","t1")] spec 1);
+ by (dres_inst_tac [("x","m1")] spec 1);
+ by (dres_inst_tac [("x","n")] spec 1);
+ by (mp_tac 1);
+ by (asm_full_simp_tac (simpset() addsimps [eq_sym_conv]) 1);
 by (simp_tac (simpset() addsimps [o_def]) 1);
 by (simp_tac (HOL_ss addsimps [subst_comp_scheme_list RS sym]) 1);
 by (rtac (gen_subst_commutes RS sym RS subst) 1);
-by (rtac (app_subst_Cons RS subst) 2);
-by (etac thin_rl 2);
-by (dres_inst_tac [("x","gen ($S1 A) t1 # $ S1 A")] spec 2);
-by (dres_inst_tac [("x","S2")] spec 2);
-by (dres_inst_tac [("x","t")] spec 2);
-by (dres_inst_tac [("x","n2")] spec 2);
-by (dres_inst_tac [("x","m2")] spec 2);
-by (ftac new_tv_W 2);
-by (assume_tac 2);
-by (dtac conjunct1 2);
-by (dtac conjunct1 2);
-by (ftac new_tv_subst_scheme_list 2);
-by (rtac new_scheme_list_le 2);
-by (rtac W_var_ge 2);
-by (assume_tac 2);
-by (assume_tac 2);
-by (etac impE 2);
-by (res_inst_tac [("A","$ S1 A")] new_tv_only_depends_on_free_tv_scheme_list 2);
-by (Simp_tac 2);
-by (Fast_tac 2);
-by (assume_tac 2);
-by (Asm_full_simp_tac 2);
+ by (rtac (app_subst_Cons RS subst) 2);
+ by (etac thin_rl 2);
+ by (dres_inst_tac [("x","gen ($S1 A) t1 # $ S1 A")] spec 2);
+ by (dres_inst_tac [("x","S2")] spec 2);
+ by (dres_inst_tac [("x","t")] spec 2);
+ by (dres_inst_tac [("x","m")] spec 2);
+ by (dres_inst_tac [("x","m1")] spec 2);
+ by (ftac new_tv_W 2);
+  by (assume_tac 2);
+ by (dtac conjunct1 2);
+ by (ftac new_tv_subst_scheme_list 2);
+  by (rtac new_scheme_list_le 2);
+   by (rtac W_var_ge 2);
+   by (assume_tac 2);
+  by (assume_tac 2);
+ by (etac impE 2);
+  by (res_inst_tac [("A","$ S1 A")] new_tv_only_depends_on_free_tv_scheme_list 2);
+   by (Simp_tac 2);
+   by (Fast_tac 2);
+  by (assume_tac 2);
+ by (Asm_full_simp_tac 2);
 by (rtac weaken_A_Int_B_eq_empty 1);
 by (rtac allI 1);
 by (strip_tac 1);
 by (rtac weaken_not_elem_A_minus_B 1);
-by (case_tac "x < m2" 1);
-by (rtac disjI2 1);
-by (rtac (free_tv_gen_cons RS subst) 1);
-by (rtac free_tv_W 1);
-by (assume_tac 1);
-by (Asm_full_simp_tac 1);
-by (assume_tac 1);
+by (case_tac "x < m1" 1);
+ by (rtac disjI2 1);
+ by (rtac (free_tv_gen_cons RS subst) 1);
+ by (rtac free_tv_W 1);
+   by (assume_tac 1);
+  by (Asm_full_simp_tac 1);
+ by (assume_tac 1);
 by (rtac disjI1 1);
 by (dtac new_tv_W 1);
 by (assume_tac 1);
-by (dtac conjunct2 1);
 by (dtac conjunct2 1);
 by (rtac new_tv_not_free_tv 1);
 by (rtac new_tv_le 1);
-by (assume_tac 2);
+ by (assume_tac 2);
 by (asm_full_simp_tac (simpset() addsimps [not_less_iff_le]) 1);
 qed_spec_mp "W_correct_lemma";
 
 (* Completeness of W w.r.t. has_type *)
 Goal "!S' A t' n. $S' A |- e :: t' --> new_tv n A -->     \