# HG changeset patch
# User nipkow
# Date 908551949 -7200
# Node ID afd75136b236358783de416b4a824852d79e1770
# Parent  8b872d546b9e5cf437bb546f99dbd48b9ddd2aa2
Mods because of: Installed trans_tac in solver of simpset().

diff -r 8b872d546b9e -r afd75136b236 src/HOL/Hoare/Examples.ML
--- 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 ***)
diff -r 8b872d546b9e -r afd75136b236 src/HOL/MiniML/W.ML
--- 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); 
diff -r 8b872d546b9e -r afd75136b236 src/HOL/W0/Type.ML
--- 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];
diff -r 8b872d546b9e -r afd75136b236 src/HOL/W0/W.ML
--- 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 *)
diff -r 8b872d546b9e -r afd75136b236 src/HOL/ex/Recdefs.ML
--- 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";