src/HOL/Hoare/Examples.ML

 by(asm_simp_tac HOL_basic_ss 1);
 by(REPEAT(etac thin_rl 1));
 by (hoare_tac Asm_full_simp_tac 1);
     by(asm_full_simp_tac (simpset() addsimps [neq_Nil_conv]) 1);
     by(Clarify_tac 1);
-    by(asm_full_simp_tac (simpset() addsimps [nth_list_update]
-                                    addSolver cut_trans_tac) 1);
+    by(asm_full_simp_tac (simpset() addsimps [nth_list_update]) 1);
    by(blast_tac (claset() addSEs [less_SucE] addIs [Suc_leI]) 1);
   br conjI 1;
    by(Clarify_tac 1);
    bd (pred_less_imp_le RS le_imp_less_Suc) 1;
    by(blast_tac (claset() addSEs [less_SucE]) 1);
   br less_imp_diff_less 1;
   by(Blast_tac 1);
  by(Clarify_tac 1);
- by(asm_simp_tac (simpset() addsimps [nth_list_update]
-                            addSolver cut_trans_tac) 1);
+ by(asm_simp_tac (simpset() addsimps [nth_list_update]) 1);
  by(Clarify_tac 1);
- by(trans_tac 1);
+ by(Simp_tac 1);
 by(Clarify_tac 1);
-by(asm_simp_tac (simpset() addSolver cut_trans_tac) 1);
+by(Asm_simp_tac 1);
 br conjI 1;
  by(Clarify_tac 1);
  br order_antisym 1;
-  by(asm_simp_tac (simpset() addSolver cut_trans_tac) 1);
- by(asm_simp_tac (simpset() addSolver cut_trans_tac) 1);
+  by(Asm_simp_tac 1);
+ by(Asm_simp_tac 1);
 by(Clarify_tac 1);
-by(asm_simp_tac (simpset() addSolver cut_trans_tac) 1);
+by(Asm_simp_tac 1);
 qed "Partition";