--- a/src/HOL/Hoare/Examples.ML Fri Nov 27 16:54:59 1998 +0100
+++ b/src/HOL/Hoare/Examples.ML Fri Nov 27 17:00:30 1998 +0100
@@ -151,8 +151,7 @@
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);
@@ -161,17 +160,16 @@
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";