src/HOL/MiniML/W.ML

 (* the resulting type variable is always greater or equal than the given one *)
 goal thy
         "!A n S t m. W e A n  = Some (S,t,m) --> n<=m";
 by (expr.induct_tac "e" 1);
 (* case Var(n) *)
-by (simp_tac (!simpset setloop (split_tac [expand_option_bind,expand_if])) 1);
+by (simp_tac (!simpset addsplits [expand_option_bind,expand_if]) 1);
 by (strip_tac 1);
 by (etac conjE 1);
 by (etac conjE 1);
 by (dtac sym 1);
 by (dtac sym 1);
 by (dtac sym 1);
 by (Asm_full_simp_tac 1);
 (* case Abs e *)
-by (simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1);
+by (simp_tac (!simpset addsplits [expand_option_bind]) 1);
 by (fast_tac (HOL_cs addDs [Suc_leD]) 1);
 (* case App e1 e2 *)
-by (simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1);
+by (simp_tac (!simpset addsplits [expand_option_bind]) 1);
 by (strip_tac 1);
 by (rename_tac "S t n1 S1 t1 n2 S2 S3 t2 m" 1);
 by (eres_inst_tac [("x","A")] allE 1);
 by (eres_inst_tac [("x","n")] allE 1);
 by (eres_inst_tac [("x","$ S A")] allE 1);

 by (etac conjE 1);
 by (res_inst_tac [("j","n1")] le_trans 1); 
 by (Asm_simp_tac 1);
 by (Asm_simp_tac 1);
 (* case LET e1 e2 *)
-by (simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1);
+by (simp_tac (!simpset addsplits [expand_option_bind]) 1);
 by (strip_tac 1);
 by (rename_tac "A n1 S t2 m1 S2 t3 m2 S3 t1 m" 1);
 by (REPEAT (etac conjE 1));
 by (REPEAT (etac allE 1));
 by (mp_tac 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 (!simpset setloop (split_tac [expand_if]) addsimps [max_def]) 1);
+by (simp_tac (!simpset addsplits [expand_if] 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 (!simpset setloop (split_tac [expand_if]) addsimps [max_def]) 1);
+by (simp_tac (!simpset addsplits [expand_if] 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);
 qed_spec_mp "new_tv_bound_typ_inst_sch";

 goal thy
      "!n A S t m. new_tv n A --> W e A n = Some (S,t,m) -->    \
 \                 new_tv m S & new_tv m t";
 by (expr.induct_tac "e" 1);
 (* case Var n *)
-by (simp_tac (!simpset setloop (split_tac [expand_option_bind,expand_if])) 1);
+by (simp_tac (!simpset addsplits [expand_option_bind,expand_if]) 1);
 by (strip_tac 1);
 by (REPEAT (etac conjE 1));
 by (rtac conjI 1);
 by (dtac sym 1);
 by (Asm_full_simp_tac 1);

 by (dtac new_tv_nth_nat_A 1);
 by (assume_tac 1);
 by (Asm_full_simp_tac 1);
 (* case Abs e *)
 by (simp_tac (!simpset addsimps [new_tv_subst,new_tv_Suc_list] 
-    setloop (split_tac [expand_option_bind])) 1);
+    addsplits [expand_option_bind]) 1);
 by (strip_tac 1);
 by (eres_inst_tac [("x","Suc n")] allE 1);
 by (eres_inst_tac [("x","(FVar n)#A")] allE 1);
 by (fast_tac (HOL_cs addss (!simpset
               addsimps [new_tv_subst,new_tv_Suc_list])) 1);
 (* case App e1 e2 *)
-by (simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1);
+by (simp_tac (!simpset addsplits [expand_option_bind]) 1);
 by (strip_tac 1);
 by (rename_tac "S t n1 S1 t1 n2 S2 S3 t2 m" 1);
 by (eres_inst_tac [("x","n")] allE 1);
 by (eres_inst_tac [("x","A")] allE 1);
 by (eres_inst_tac [("x","S")] allE 1);

    new_tv_subst_le,new_tv_le] addss !simpset) 1);
 by (fast_tac (HOL_cs addDs [W_var_geD] addIs
      [new_scheme_list_le,new_tv_subst_scheme_list,new_tv_le]
      addss (!simpset)) 1);
 (* case LET e1 e2 *)
-by (simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1);
+by (simp_tac (!simpset addsplits [expand_option_bind]) 1);
 by (strip_tac 1);
 by (rename_tac "n1 A S1 t1 n2 S2 t2 m2 S t m" 1);
 by (REPEAT (etac conjE 1));
 by (eres_inst_tac [("x","n1")] allE 1);
 by (eres_inst_tac [("x","A")] allE 1);

      "!n A S t m v. W e A n = Some (S,t,m) -->            \
 \         (v:free_tv S | v:free_tv t) --> v<n --> v:free_tv A";
 by (expr.induct_tac "e" 1);
 (* case Var n *)
 by (simp_tac (!simpset addsimps
-    [free_tv_subst] setloop (split_tac [expand_option_bind,expand_if])) 1);
+    [free_tv_subst] addsplits [expand_option_bind,expand_if]) 1);
 by (strip_tac 1);
 by (REPEAT (etac conjE 1));
 by (hyp_subst_tac 1);
 by (asm_full_simp_tac (!simpset addsimps [dom_def,cod_def,id_subst_def]) 1);
 by (case_tac "v : free_tv (nth nat A)" 1);

 by (etac exE 1);
 by (rotate_tac 3 1);
 by (Asm_full_simp_tac 1);
 (* case Abs e *)
 by (asm_full_simp_tac (!simpset addsimps
-    [free_tv_subst] setloop (split_tac [expand_option_bind]) delsimps all_simps) 1);
+    [free_tv_subst] addsplits [expand_option_bind] delsimps all_simps) 1);
 by (strip_tac 1);
 by (rename_tac "S t n1 S1 t1 m v" 1);
 by (eres_inst_tac [("x","Suc n")] allE 1);
 by (eres_inst_tac [("x","FVar n # A")] allE 1);
 by (eres_inst_tac [("x","S")] allE 1);

 by (eres_inst_tac [("x","n1")] allE 1);
 by (eres_inst_tac [("x","v")] allE 1);
 by (best_tac (HOL_cs addIs [cod_app_subst]
                      addss (!simpset addsimps [less_Suc_eq])) 1);
 (* case App e1 e2 *)
-by (simp_tac (!simpset setloop (split_tac [expand_option_bind]) delsimps all_simps) 1);
+by (simp_tac (!simpset addsplits [expand_option_bind] delsimps all_simps) 1);
 by (strip_tac 1); 
 by (rename_tac "S t n1 S1 t1 n2 S2 S3 t2 m v" 1);
 by (eres_inst_tac [("x","n")] allE 1);
 by (eres_inst_tac [("x","A")] allE 1);
 by (eres_inst_tac [("x","S")] allE 1);

     free_tv_app_subst_te RS subsetD,free_tv_app_subst_scheme_list RS subsetD,
     less_le_trans,subsetD]
   addEs [UnE]
   addss !simpset) 1);
 (* LET e1 e2 *)
-by (simp_tac (!simpset setloop (split_tac [expand_option_bind]) delsimps all_simps) 1);
+by (simp_tac (!simpset addsplits [expand_option_bind] delsimps all_simps) 1);
 by (strip_tac 1); 
 by (rename_tac "nat A S1 t1 n2 S2 t2 m2 S t m v" 1);
 by (eres_inst_tac [("x","nat")] allE 1);
 by (eres_inst_tac [("x","A")] allE 1);
 by (eres_inst_tac [("x","S1")] allE 1);

 (* correctness of W with respect to has_type *)
 goal W.thy
         "!A S t m n . new_tv n A --> Some (S,t,m) = W e A n --> $S A |- e :: t";
 by (expr.induct_tac "e" 1);
 (* case Var n *)
-by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
+by (asm_full_simp_tac (!simpset addsplits [expand_if]) 1);
 by (strip_tac 1);
 by (rtac has_type.VarI 1);
 by (Simp_tac 1);
 by (simp_tac (!simpset addsimps [is_bound_typ_instance]) 1);
 by (rtac exI 1);
 by (rtac refl 1);
 (* case Abs e *)
 by (asm_full_simp_tac (!simpset addsimps [app_subst_list]
-                        setloop (split_tac [expand_option_bind])) 1);
+                        addsplits [expand_option_bind]) 1);
 by (strip_tac 1);
 by (eres_inst_tac [("x","(mk_scheme (TVar n)) # A")] allE 1);
 by (Asm_full_simp_tac 1);
 by (rtac has_type.AbsI 1);
 by (dtac (le_refl RS le_SucI RS new_scheme_list_le) 1);

 by (etac impE 1);
 by (mp_tac 2);
 by (Asm_simp_tac 1);
 by (assume_tac 1);
 (* case App e1 e2 *)
-by (simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1);
+by (simp_tac (!simpset addsplits [expand_option_bind]) 1);
 by (strip_tac 1);
 by (rename_tac "S1 t1 n1 S2 t2 n2 S3" 1);
 by (res_inst_tac [("t2.0","$ S3 t2")] has_type.AppI 1);
 by (res_inst_tac [("S1","S3")] (app_subst_TVar RS subst) 1);
 by (rtac (app_subst_Fun RS subst) 1);

 by (etac thin_rl 1);
 by (mp_tac 1);
 by (mp_tac 1);
 by (assume_tac 1);
 (* case Let e1 e2 *)
-by (simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1);
+by (simp_tac (!simpset addsplits [expand_option_bind]) 1);
 by (strip_tac 1);
 by (rename_tac "w q m1 S1 t1 m2 S2 t n2" 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);

 \             (? S t. (? m. W e A n = Some (S,t,m)) &  \
 \                     (? R. $S' A = $R ($S A) & t' = $R t))";
 by (expr.induct_tac "e" 1);
 (* case Var n *)
 by (strip_tac 1);
-by (simp_tac (!simpset addcongs [conj_cong] 
-    setloop (split_tac [expand_if])) 1);
+by (simp_tac (!simpset addcongs [conj_cong] addsplits [expand_if]) 1);
 by (eresolve_tac has_type_casesE 1); 
 by (asm_full_simp_tac (!simpset addsimps [is_bound_typ_instance]) 1);
 by (etac exE 1);
 by (hyp_subst_tac 1);
 by (rename_tac "S" 1);

 by (eres_inst_tac [("x","(FVar n)#A")] allE 1);
 by (eres_inst_tac [("x","t2")] allE 1);
 by (eres_inst_tac [("x","Suc n")] allE 1);
 by (best_tac (HOL_cs addSDs [mk_scheme_injective] 
                   addss (!simpset addcongs [conj_cong] 
-                                setloop (split_tac [expand_option_bind]))) 1);
+                                addsplits [expand_option_bind])) 1);
 (** LEVEL 19 **)
 
 (* case App e1 e2 *)
 by (strip_tac 1);
 by (eresolve_tac has_type_casesE 1);

 by (best_tac (HOL_cs addDs [new_tv_W,sym RS W_var_geD,
     new_tv_not_free_tv,new_tv_le]) 3);
 by (case_tac "na:free_tv Sa" 2);
 (* n1 ~: free_tv S1 *)
 by (forward_tac [not_free_impl_id] 3);
-by (asm_simp_tac (!simpset 
-    setloop (split_tac [expand_if])) 3);
+by (asm_simp_tac (!simpset addsplits [expand_if]) 3);
 (* na : free_tv Sa *)
 by (dres_inst_tac [("A1","$ S A")] (subst_comp_scheme_list RSN (2,trans)) 2);
 by (dtac eq_subst_scheme_list_eq_free 2);
 by (fast_tac (HOL_cs addIs [free_tv_W,free_tv_le_new_tv] addDs [new_tv_W]) 2);
 by (Asm_simp_tac 2); 
 by (case_tac "na:dom Sa" 2);
 (* na ~: dom Sa *)
-by (asm_full_simp_tac (!simpset addsimps [dom_def] 
-    setloop (split_tac [expand_if])) 3);
+by (asm_full_simp_tac (!simpset addsimps [dom_def] addsplits [expand_if]) 3);
 (* na : dom Sa *)
 by (rtac eq_free_eq_subst_te 2);
 by (strip_tac 2);
 by (subgoal_tac "nb ~= ma" 2);
 by ((forward_tac [new_tv_W] 3) THEN (atac 3));

 by (dtac new_tv_subst_scheme_list 3);
 by (fast_tac (HOL_cs addIs [new_scheme_list_le] addDs [sym RS W_var_geD]) 3);
 by (fast_tac (set_cs addDs [new_tv_W,new_tv_not_free_tv] addss 
     (!simpset addsimps [cod_def,free_tv_subst])) 3);
 by (fast_tac (set_cs addss (!simpset addsimps [cod_def,free_tv_subst] 
-    setloop (split_tac [expand_if]))) 2);
+                                     addsplits [expand_if])) 2);
 by (Simp_tac 2);  
 by (rtac eq_free_eq_subst_te 2);
 by (strip_tac 2 );
 by (subgoal_tac "na ~= ma" 2);
 by ((forward_tac [new_tv_W] 3) THEN (atac 3));
 by (etac conjE 3);
 by (dtac (sym RS W_var_geD) 3);
 by (fast_tac (HOL_cs addDs [new_scheme_list_le,new_tv_subst_scheme_list,new_tv_W,new_tv_not_free_tv]) 3);
 by (case_tac "na: free_tv t - free_tv Sa" 2);
 (* case na ~: free_tv t - free_tv Sa *)
-by ( asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 3);
+by ( asm_full_simp_tac (!simpset addsplits [expand_if]) 3);
 by (Fast_tac 3);
 (* case na : free_tv t - free_tv Sa *)
-by ( asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 2);
+by ( asm_full_simp_tac (!simpset addsplits [expand_if]) 2);
 by (dres_inst_tac [("A1","$ S A")] (subst_comp_scheme_list RSN (2,trans)) 2);
 by (dtac eq_subst_scheme_list_eq_free 2);
 by (fast_tac (HOL_cs addIs [free_tv_W,free_tv_le_new_tv] addDs [new_tv_W]) 2);
 (** LEVEL 75 **)
 by (asm_full_simp_tac (!simpset addsimps [free_tv_subst,dom_def]) 2);
-by (asm_simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1); 
+by (asm_simp_tac (!simpset addsplits [expand_option_bind]) 1); 
 by (safe_tac HOL_cs );
 by (dtac mgu_Some 1);
 by ( fast_tac (HOL_cs addss !simpset) 1);
 (** LEVEL 80 *)
 by ((dtac mgu_mg 1) THEN (atac 1));

 by (dtac (free_tv_app_subst_scheme_list RS subsetD) 2);
 by (fast_tac (set_cs addDs [sym RS W_var_geD,new_scheme_list_le,codD,
     new_tv_not_free_tv]) 2);
 by (case_tac "na: free_tv t - free_tv Sa" 1);
 (* case na ~: free_tv t - free_tv Sa *)
-by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 2);
+by (asm_full_simp_tac (!simpset addsplits [expand_if]) 2);
 (* case na : free_tv t - free_tv Sa *)
-by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
+by (asm_full_simp_tac (!simpset addsplits [expand_if]) 1);
 by (dtac (free_tv_app_subst_scheme_list RS subsetD) 1);
 by (fast_tac (set_cs addDs [codD,subst_comp_scheme_list RSN (2,trans),
     eq_subst_scheme_list_eq_free] addss ((!simpset addsimps 
     [free_tv_subst,dom_def]))) 1);
 by (Fast_tac 1);