Adapted to new simplifier.

--- a/src/ZF/ArithSimp.thy	Mon Sep 30 16:44:00 2002 +0200
+++ b/src/ZF/ArithSimp.thy	Mon Sep 30 16:47:03 2002 +0200
@@ -119,7 +119,7 @@
      "[| 0<n; n le m;  m:nat |] ==> raw_mod (m, n) = raw_mod (m#-n, n)"
 apply (frule lt_nat_in_nat, erule nat_succI)
 apply (rule raw_mod_def [THEN def_transrec, THEN trans])
-apply (simp add: div_termination [THEN ltD] not_lt_iff_le [THEN iffD2], blast)
+apply (simp (no_asm_simp) add: div_termination [THEN ltD] not_lt_iff_le [THEN iffD2], blast)
 done
 
 
@@ -160,7 +160,7 @@
 prefer 2 apply blast
 apply (frule lt_nat_in_nat, erule nat_succI)
 apply (rule raw_div_def [THEN def_transrec, THEN trans])
-apply (simp add: div_termination [THEN ltD] not_lt_iff_le [THEN iffD2] ) 
+apply (simp (no_asm_simp) add: div_termination [THEN ltD] not_lt_iff_le [THEN iffD2] ) 
 done
 
 lemma div_geq [simp]:

--- a/src/ZF/Constructible/Relative.thy	Mon Sep 30 16:44:00 2002 +0200
+++ b/src/ZF/Constructible/Relative.thy	Mon Sep 30 16:47:03 2002 +0200
@@ -967,7 +967,7 @@
 apply (simp add: powerset_def) 
 apply (rule equalityI, clarify, simp)
  apply (frule transM, assumption) 
- apply (frule transM, assumption, simp) 
+ apply (frule transM, assumption, simp (no_asm_simp))
  apply blast 
 apply clarify
 apply (frule transM, assumption, force) 

--- a/src/ZF/Constructible/Wellorderings.thy	Mon Sep 30 16:44:00 2002 +0200
+++ b/src/ZF/Constructible/Wellorderings.thy	Mon Sep 30 16:47:03 2002 +0200
@@ -408,8 +408,7 @@
 
 lemma (in M_basic) omap_yields_Ord:
      "[| omap(M,A,r,f); \<langle>a,x\<rangle> \<in> f; M(a); M(x) |]  ==> Ord(x)"
-apply (simp add: omap_def, blast) 
-done
+  by (simp add: omap_def)
 
 lemma (in M_basic) otype_iff:
      "[| otype(M,A,r,i); M(A); M(r); M(i) |] 

--- a/src/ZF/List.thy	Mon Sep 30 16:44:00 2002 +0200
+++ b/src/ZF/List.thy	Mon Sep 30 16:47:03 2002 +0200
@@ -1089,7 +1089,6 @@
 apply (simp add: nth_append le_iff split add: nat_diff_split)
 apply (auto dest!: not_lt_imp_le 
             simp add: nth_append diff_self_eq_0 less_diff_conv add_commute)
-apply (drule_tac j = x in lt_trans2, auto)
 done
 
 lemma take_upt [rule_format,simp]:

--- a/src/ZF/Order.thy	Mon Sep 30 16:44:00 2002 +0200
+++ b/src/ZF/Order.thy	Mon Sep 30 16:47:03 2002 +0200
@@ -247,7 +247,7 @@
 (*Needed?  But ord_iso_converse is!*)
 lemma ord_iso_apply:
     "[| f: ord_iso(A,r,B,s);  <x,y>: r;  x:A;  y:A |] ==> <f`x, f`y> : s"
-by (simp add: ord_iso_def, blast)
+by (simp add: ord_iso_def)
 
 lemma ord_iso_converse:
     "[| f: ord_iso(A,r,B,s);  <x,y>: s;  x:B;  y:B |]

--- a/src/ZF/OrderType.thy	Mon Sep 30 16:44:00 2002 +0200
+++ b/src/ZF/OrderType.thy	Mon Sep 30 16:47:03 2002 +0200
@@ -520,10 +520,10 @@
 done
 
 lemma oadd_lt_cancel2: "[| i++j < i++k;  Ord(j) |] ==> j<k"
-apply (simp add: oadd_eq_if_raw_oadd split add: split_if_asm)
+apply (simp (asm_lr) add: oadd_eq_if_raw_oadd split add: split_if_asm)
  prefer 2
  apply (frule_tac i = i and j = j in oadd_le_self)
- apply (simp add: oadd_def ordify_def lt_Ord not_lt_iff_le [THEN iff_sym])
+ apply (simp (asm_lr) add: oadd_def ordify_def lt_Ord not_lt_iff_le [THEN iff_sym])
 apply (rule Ord_linear_lt, auto) 
 apply (simp_all add: raw_oadd_eq_oadd)
 apply (blast dest: oadd_lt_mono2 elim: lt_irrefl lt_asym)+

--- a/src/ZF/Perm.thy	Mon Sep 30 16:44:00 2002 +0200
+++ b/src/ZF/Perm.thy	Mon Sep 30 16:47:03 2002 +0200
@@ -467,7 +467,6 @@
 apply (rule_tac d = "%z. if z:B then converse (f) `z else converse (g) `z" 
        in lam_injective)
 apply (auto simp add: inj_is_fun [THEN apply_type])
-apply (blast intro: inj_is_fun [THEN apply_type])
 done
 
 lemma surj_disjoint_Un: 

--- a/src/ZF/equalities.thy	Mon Sep 30 16:44:00 2002 +0200
+++ b/src/ZF/equalities.thy	Mon Sep 30 16:47:03 2002 +0200
@@ -491,7 +491,7 @@
 apply (simp add: Inter_def)
 apply (subgoal_tac "ALL x:A. x~=0")
 prefer 2 apply blast
-apply force
+apply (tactic "first_best_tac (claset() addss' simpset()) 1")
 done
 
 lemma INT_UN_eq: "(ALL x:A. B(x) ~= 0)