Mods because of: Installed trans_tac in solver of simpset().
--- a/src/HOL/Hoare/Examples.ML Fri Oct 16 17:32:06 1998 +0200
+++ b/src/HOL/Hoare/Examples.ML Fri Oct 16 17:32:29 1998 +0200
@@ -64,12 +64,11 @@
\ DO b := b*a; a := a-1 OD \
\ {b = fac A}";
by (hoare_tac Asm_full_simp_tac 1);
-by Safe_tac;
+by (Clarify_tac 1);
by (exhaust_tac "a" 1);
by (ALLGOALS
(asm_simp_tac
(simpset() addsimps [add_mult_distrib,add_mult_distrib2,mult_assoc])));
-by (Fast_tac 1);
qed"factorial";
(*** LISTS ***)
--- a/src/HOL/MiniML/W.ML Fri Oct 16 17:32:06 1998 +0200
+++ b/src/HOL/MiniML/W.ML Fri Oct 16 17:32:29 1998 +0200
@@ -230,7 +230,7 @@
free_tv_app_subst_te RS subsetD,free_tv_app_subst_scheme_list RS subsetD,
less_le_trans,subsetD]
addEs [UnE]
- addss simpset()) 1);
+ addss (simpset() setSolver unsafe_solver)) 1);
(* LET e1 e2 *)
by (simp_tac (simpset() addsplits [split_option_bind] delsimps all_simps) 1);
by (strip_tac 1);
--- a/src/HOL/W0/Type.ML Fri Oct 16 17:32:06 1998 +0200
+++ b/src/HOL/W0/Type.ML Fri Oct 16 17:32:29 1998 +0200
@@ -190,11 +190,9 @@
Goal
"[| n<=m; new_tv n (s::subst) |] ==> new_tv m s";
by (asm_full_simp_tac (simpset() addsimps [new_tv_subst]) 1);
-by (rtac conjI 1);
-by (slow_tac (HOL_cs addIs [le_trans]) 1);
-by (safe_tac HOL_cs );
+by (Clarify_tac 1);
by (res_inst_tac [("P","l < n"),("Q","n <= l")] disjE 1);
-by (fast_tac (HOL_cs addss (HOL_ss addsimps [le_def])) 1);
+by (Clarify_tac 1);
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [new_tv_le])) );
qed "new_tv_subst_le";
Addsimps [lessI RS less_imp_le RS new_tv_subst_le];
--- a/src/HOL/W0/W.ML Fri Oct 16 17:32:06 1998 +0200
+++ b/src/HOL/W0/W.ML Fri Oct 16 17:32:29 1998 +0200
@@ -209,7 +209,8 @@
free_tv_app_subst_tel RS subsetD,
less_le_trans,subsetD]
addSEs [UnE]
- addss simpset()) 1);
+ addss (simpset() setSolver unsafe_solver)) 1);
+(* builtin arithmetic in simpset messes things up *)
qed_spec_mp "free_tv_W";
(* Completeness of W w.r.t. has_type *)
--- a/src/HOL/ex/Recdefs.ML Fri Oct 16 17:32:06 1998 +0200
+++ b/src/HOL/ex/Recdefs.ML Fri Oct 16 17:32:29 1998 +0200
@@ -23,7 +23,6 @@
Goal "g x < Suc x";
by (res_inst_tac [("u","x")] g.induct 1);
by Auto_tac;
-by (trans_tac 1);
qed "g_terminates";
Goal "g x = 0";