diff -r 9f1eaab75e8c -r 771b1f6422a8 src/ZF/OrderType.ML
--- a/src/ZF/OrderType.ML	Mon Nov 03 12:22:43 1997 +0100
+++ b/src/ZF/OrderType.ML	Mon Nov 03 12:24:13 1997 +0100
@@ -18,7 +18,7 @@
 by (rtac well_ordI 1);
 by (rtac (wf_Memrel RS wf_imp_wf_on) 1);
 by (resolve_tac [prem RS ltE] 1);
-by (asm_simp_tac (!simpset addsimps [linear_def, Memrel_iff,
+by (asm_simp_tac (simpset() addsimps [linear_def, Memrel_iff,
                                   [ltI, prem] MRS lt_trans2 RS ltD]) 1);
 by (REPEAT (resolve_tac [ballI, Ord_linear] 1));
 by (REPEAT (eresolve_tac [asm_rl, Ord_in_Ord] 1));
@@ -31,8 +31,8 @@
   The smaller ordinal is an initial segment of the larger *)
 goalw OrderType.thy [pred_def, lt_def]
     "!!i j. j<i ==> pred(i, j, Memrel(i)) = j";
-by (asm_simp_tac (!simpset addsimps [Memrel_iff]) 1);
-by (blast_tac (!claset addIs [Ord_trans]) 1);
+by (asm_simp_tac (simpset() addsimps [Memrel_iff]) 1);
+by (blast_tac (claset() addIs [Ord_trans]) 1);
 qed "lt_pred_Memrel";
 
 goalw OrderType.thy [pred_def,Memrel_def] 
@@ -46,10 +46,10 @@
 by (etac ltE 1);
 by (rtac (well_ord_Memrel RS well_ord_iso_predE) 1 THEN
     assume_tac 3 THEN assume_tac 1);
-by (asm_full_simp_tac (!simpset addsimps [ord_iso_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [ord_iso_def]) 1);
 (*Combining the two simplifications causes looping*)
-by (asm_simp_tac (!simpset addsimps [Memrel_iff]) 1);
-by (fast_tac (!claset addSEs [bij_is_fun RS apply_type] addEs [Ord_trans]) 1);
+by (asm_simp_tac (simpset() addsimps [Memrel_iff]) 1);
+by (fast_tac (claset() addSEs [bij_is_fun RS apply_type] addEs [Ord_trans]) 1);
 qed "Ord_iso_implies_eq_lemma";
 
 (*Kunen's Theorem 7.3 (ii), page 16.  Isomorphic ordinals are equal*)
@@ -79,7 +79,7 @@
 by (Asm_simp_tac 1);
 by (etac (wfrec_on RS trans) 1);
 by (assume_tac 1);
-by (asm_simp_tac (!simpset addsimps [subset_iff, image_lam,
+by (asm_simp_tac (simpset() addsimps [subset_iff, image_lam,
                                   vimage_singleton_iff]) 1);
 qed "ordermap_eq_image";
 
@@ -87,7 +87,7 @@
 goal OrderType.thy 
     "!!r. [| wf[A](r);  x:A |] ==> \
 \         ordermap(A,r) ` x = {ordermap(A,r)`y . y : pred(A,x,r)}";
-by (asm_simp_tac (!simpset addsimps [ordermap_eq_image, pred_subset, 
+by (asm_simp_tac (simpset() addsimps [ordermap_eq_image, pred_subset, 
                                   ordermap_type RS image_fun]) 1);
 qed "ordermap_pred_unfold";
 
@@ -103,24 +103,24 @@
 
 goalw OrderType.thy [well_ord_def, tot_ord_def, part_ord_def]
     "!!r. [| well_ord(A,r);  x:A |] ==> Ord(ordermap(A,r) ` x)";
-by (safe_tac (!claset));
+by (safe_tac (claset()));
 by (wf_on_ind_tac "x" [] 1);
-by (asm_simp_tac (!simpset addsimps [ordermap_pred_unfold]) 1);
+by (asm_simp_tac (simpset() addsimps [ordermap_pred_unfold]) 1);
 by (rtac (Ord_is_Transset RSN (2,OrdI)) 1);
 by (rewrite_goals_tac [pred_def,Transset_def]);
 by (Blast_tac 2);
-by (safe_tac (!claset));
+by (safe_tac (claset()));
 by (ordermap_elim_tac 1);
-by (fast_tac (!claset addSEs [trans_onD]) 1);
+by (fast_tac (claset() addSEs [trans_onD]) 1);
 qed "Ord_ordermap";
 
 goalw OrderType.thy [ordertype_def]
     "!!r. well_ord(A,r) ==> Ord(ordertype(A,r))";
 by (stac ([ordermap_type, subset_refl] MRS image_fun) 1);
 by (rtac (Ord_is_Transset RSN (2,OrdI)) 1);
-by (blast_tac (!claset addIs [Ord_ordermap]) 2);
+by (blast_tac (claset() addIs [Ord_ordermap]) 2);
 by (rewrite_goals_tac [Transset_def,well_ord_def]);
-by (safe_tac (!claset));
+by (safe_tac (claset()));
 by (ordermap_elim_tac 1);
 by (Blast_tac 1);
 qed "Ord_ordertype";
@@ -139,9 +139,9 @@
 goalw OrderType.thy [well_ord_def, tot_ord_def]
     "!!r. [| ordermap(A,r)`w : ordermap(A,r)`x;  well_ord(A,r);  \
 \            w: A; x: A |] ==> <w,x>: r";
-by (safe_tac (!claset));
+by (safe_tac (claset()));
 by (linear_case_tac 1);
-by (blast_tac (!claset addSEs [mem_not_refl RS notE]) 1);
+by (blast_tac (claset() addSEs [mem_not_refl RS notE]) 1);
 by (dtac ordermap_mono 1);
 by (REPEAT_SOME assume_tac);
 by (etac mem_asym 1);
@@ -154,10 +154,10 @@
 
 goalw OrderType.thy [well_ord_def, tot_ord_def, bij_def, inj_def]
     "!!r. well_ord(A,r) ==> ordermap(A,r) : bij(A, ordertype(A,r))";
-by (fast_tac (!claset addSIs [ordermap_type, ordermap_surj]
+by (fast_tac (claset() addSIs [ordermap_type, ordermap_surj]
                       addEs [linearE]
                       addDs [ordermap_mono]
-                      addss (!simpset addsimps [mem_not_refl])) 1);
+                      addss (simpset() addsimps [mem_not_refl])) 1);
 qed "ordermap_bij";
 
 (*** Isomorphisms involving ordertype ***)
@@ -165,10 +165,10 @@
 goalw OrderType.thy [ord_iso_def]
  "!!r. well_ord(A,r) ==> \
 \      ordermap(A,r) : ord_iso(A,r, ordertype(A,r), Memrel(ordertype(A,r)))";
-by (safe_tac (!claset addSEs [well_ord_is_wf]
+by (safe_tac (claset() addSEs [well_ord_is_wf]
 		      addSIs [ordermap_type RS apply_type,
 			      ordermap_mono, ordermap_bij]));
-by (blast_tac (!claset addSDs [converse_ordermap_mono]) 1);
+by (blast_tac (claset() addSDs [converse_ordermap_mono]) 1);
 qed "ordertype_ord_iso";
 
 goal OrderType.thy
@@ -177,7 +177,7 @@
 by (forward_tac [well_ord_ord_iso] 1 THEN assume_tac 1);
 by (rtac Ord_iso_implies_eq 1
     THEN REPEAT (etac Ord_ordertype 1));
-by (deepen_tac (!claset addIs  [ord_iso_trans, ord_iso_sym]
+by (deepen_tac (claset() addIs  [ord_iso_trans, ord_iso_sym]
                       addSEs [ordertype_ord_iso]) 0 1);
 qed "ordertype_eq";
 
@@ -202,8 +202,8 @@
 by (rtac ord_iso_trans 1);
 by (eresolve_tac [le_well_ord_Memrel RS ordertype_ord_iso] 2);
 by (resolve_tac [id_bij RS ord_isoI] 1);
-by (asm_simp_tac (!simpset addsimps [id_conv, Memrel_iff]) 1);
-by (fast_tac (!claset addEs [ltE, Ord_in_Ord, Ord_trans]) 1);
+by (asm_simp_tac (simpset() addsimps [id_conv, Memrel_iff]) 1);
+by (fast_tac (claset() addEs [ltE, Ord_in_Ord, Ord_trans]) 1);
 qed "le_ordertype_Memrel";
 
 (*"Ord(i) ==> ordertype(i, Memrel(i)) = i"*)
@@ -230,15 +230,15 @@
 \         ordermap(pred(A,y,r), r) ` z = ordermap(A, r) ` z";
 by (forward_tac [[well_ord_is_wf, pred_subset] MRS wf_on_subset_A] 1);
 by (wf_on_ind_tac "z" [] 1);
-by (safe_tac (!claset addSEs [predE]));
+by (safe_tac (claset() addSEs [predE]));
 by (asm_simp_tac
-    (!simpset addsimps [ordermap_pred_unfold, well_ord_is_wf, pred_iff]) 1);
+    (simpset() addsimps [ordermap_pred_unfold, well_ord_is_wf, pred_iff]) 1);
 (*combining these two simplifications LOOPS! *)
-by (asm_simp_tac (!simpset addsimps [pred_pred_eq]) 1);
-by (asm_full_simp_tac (!simpset addsimps [pred_def]) 1);
+by (asm_simp_tac (simpset() addsimps [pred_pred_eq]) 1);
+by (asm_full_simp_tac (simpset() addsimps [pred_def]) 1);
 by (rtac (refl RSN (2,RepFun_cong)) 1);
 by (dtac well_ord_is_trans_on 1);
-by (fast_tac (!claset addSEs [trans_onD]) 1);
+by (fast_tac (claset() addSEs [trans_onD]) 1);
 qed "ordermap_pred_eq_ordermap";
 
 goalw OrderType.thy [ordertype_def]
@@ -251,9 +251,9 @@
 goal OrderType.thy
     "!!r. [| well_ord(A,r);  x:A |] ==>             \
 \         ordertype(pred(A,x,r),r) <= ordertype(A,r)";
-by (asm_simp_tac (!simpset addsimps [ordertype_unfold, 
+by (asm_simp_tac (simpset() addsimps [ordertype_unfold, 
                   pred_subset RSN (2, well_ord_subset)]) 1);
-by (fast_tac (!claset addIs [ordermap_pred_eq_ordermap]
+by (fast_tac (claset() addIs [ordermap_pred_eq_ordermap]
                       addEs [predE]) 1);
 qed "ordertype_pred_subset";
 
@@ -273,10 +273,10 @@
     "!!A r. well_ord(A,r) ==>  \
 \           ordertype(A,r) = {ordertype(pred(A,x,r),r). x:A}";
 by (rtac equalityI 1);
-by (safe_tac (!claset addSIs [ordertype_pred_lt RS ltD]));
+by (safe_tac (claset() addSIs [ordertype_pred_lt RS ltD]));
 by (fast_tac
-    (!claset addss
-     (!simpset addsimps [ordertype_def, 
+    (claset() addss
+     (simpset() addsimps [ordertype_def, 
                       well_ord_is_wf RS ordermap_eq_image, 
                       ordermap_type RS image_fun, 
                       ordermap_pred_eq_ordermap, 
@@ -292,15 +292,15 @@
 by (rtac conjI 1);
 by (etac well_ord_Memrel 1);
 by (rewrite_goals_tac [Ord_def, Transset_def, pred_def, Memrel_def]);
-by (Blast.depth_tac (!claset) 8 1);
+by (Blast.depth_tac (claset()) 8 1);
 qed "Ord_is_Ord_alt";
 
 (*proof by lcp*)
 goalw OrderType.thy [Ord_alt_def, Ord_def, Transset_def, well_ord_def, 
                      tot_ord_def, part_ord_def, trans_on_def] 
     "!!i. Ord_alt(i) ==> Ord(i)";
-by (asm_full_simp_tac (!simpset addsimps [Memrel_iff, pred_Memrel]) 1);
-by (blast_tac (!claset addSEs [equalityE]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Memrel_iff, pred_Memrel]) 1);
+by (blast_tac (claset() addSEs [equalityE]) 1);
 qed "Ord_alt_is_Ord";
 
 
@@ -312,7 +312,7 @@
 
 goal OrderType.thy "(lam z:A+0. case(%x. x, %y. y, z)) : bij(A+0, A)";
 by (res_inst_tac [("d", "Inl")] lam_bijective 1);
-by (safe_tac (!claset));
+by (safe_tac (claset()));
 by (ALLGOALS Asm_simp_tac);
 qed "bij_sum_0";
 
@@ -320,12 +320,12 @@
  "!!A r. well_ord(A,r) ==> ordertype(A+0, radd(A,r,0,s)) = ordertype(A,r)";
 by (resolve_tac [bij_sum_0 RS ord_isoI RS ordertype_eq] 1);
 by (assume_tac 2);
-by (fast_tac (!claset addss (!simpset addsimps [radd_Inl_iff, Memrel_iff])) 1);
+by (fast_tac (claset() addss (simpset() addsimps [radd_Inl_iff, Memrel_iff])) 1);
 qed "ordertype_sum_0_eq";
 
 goal OrderType.thy "(lam z:0+A. case(%x. x, %y. y, z)) : bij(0+A, A)";
 by (res_inst_tac [("d", "Inr")] lam_bijective 1);
-by (safe_tac (!claset));
+by (safe_tac (claset()));
 by (ALLGOALS Asm_simp_tac);
 qed "bij_0_sum";
 
@@ -333,7 +333,7 @@
  "!!A r. well_ord(A,r) ==> ordertype(0+A, radd(0,s,A,r)) = ordertype(A,r)";
 by (resolve_tac [bij_0_sum RS ord_isoI RS ordertype_eq] 1);
 by (assume_tac 2);
-by (fast_tac (!claset addss (!simpset addsimps [radd_Inr_iff, Memrel_iff])) 1);
+by (fast_tac (claset() addss (simpset() addsimps [radd_Inr_iff, Memrel_iff])) 1);
 qed "ordertype_0_sum_eq";
 
 (** Initial segments of radd.  Statements by Grabczewski **)
@@ -344,10 +344,10 @@
 \        (lam x:pred(A,a,r). Inl(x))    \
 \        : bij(pred(A,a,r), pred(A+B, Inl(a), radd(A,r,B,s)))";
 by (res_inst_tac [("d", "case(%x. x, %y. y)")] lam_bijective 1);
-by (safe_tac (!claset));
+by (safe_tac (claset()));
 by (ALLGOALS
     (asm_full_simp_tac 
-     (!simpset addsimps [radd_Inl_iff, radd_Inr_Inl_iff])));
+     (simpset() addsimps [radd_Inl_iff, radd_Inr_Inl_iff])));
 qed "pred_Inl_bij";
 
 goal OrderType.thy
@@ -356,7 +356,7 @@
 \        ordertype(pred(A,a,r), r)";
 by (resolve_tac [pred_Inl_bij RS ord_isoI RS ord_iso_sym RS ordertype_eq] 1);
 by (REPEAT_FIRST (ares_tac [pred_subset, well_ord_subset]));
-by (asm_full_simp_tac (!simpset addsimps [radd_Inl_iff, pred_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [radd_Inl_iff, pred_def]) 1);
 qed "ordertype_pred_Inl_eq";
 
 goalw OrderType.thy [pred_def, id_def]
@@ -364,7 +364,7 @@
 \        id(A+pred(B,b,s))      \
 \        : bij(A+pred(B,b,s), pred(A+B, Inr(b), radd(A,r,B,s)))";
 by (res_inst_tac [("d", "%z. z")] lam_bijective 1);
-by (safe_tac (!claset));
+by (safe_tac (claset()));
 by (ALLGOALS (Asm_full_simp_tac));
 qed "pred_Inr_bij";
 
@@ -373,7 +373,7 @@
 \        ordertype(pred(A+B, Inr(b), radd(A,r,B,s)), radd(A,r,B,s)) = \
 \        ordertype(A+pred(B,b,s), radd(A,r,pred(B,b,s),s))";
 by (resolve_tac [pred_Inr_bij RS ord_isoI RS ord_iso_sym RS ordertype_eq] 1);
-by (fast_tac (!claset addss (!simpset addsimps [pred_def, id_def])) 2);
+by (fast_tac (claset() addss (simpset() addsimps [pred_def, id_def])) 2);
 by (REPEAT_FIRST (ares_tac [well_ord_radd, pred_subset, well_ord_subset]));
 qed "ordertype_pred_Inr_eq";
 
@@ -387,12 +387,12 @@
 (** Ordinal addition with zero **)
 
 goalw OrderType.thy [oadd_def] "!!i. Ord(i) ==> i++0 = i";
-by (asm_simp_tac (!simpset addsimps [Memrel_0, ordertype_sum_0_eq, 
+by (asm_simp_tac (simpset() addsimps [Memrel_0, ordertype_sum_0_eq, 
                                   ordertype_Memrel, well_ord_Memrel]) 1);
 qed "oadd_0";
 
 goalw OrderType.thy [oadd_def] "!!i. Ord(i) ==> 0++i = i";
-by (asm_simp_tac (!simpset addsimps [Memrel_0, ordertype_0_sum_eq, 
+by (asm_simp_tac (simpset() addsimps [Memrel_0, ordertype_0_sum_eq, 
                                   ordertype_Memrel, well_ord_Memrel]) 1);
 qed "oadd_0_left";
 
@@ -406,7 +406,7 @@
 by (rtac ltI 1);
 by (REPEAT (ares_tac [Ord_ordertype, well_ord_radd, well_ord_Memrel] 2));
 by (asm_simp_tac 
-    (!simpset addsimps [ordertype_pred_unfold, 
+    (simpset() addsimps [ordertype_pred_unfold, 
                         well_ord_radd, well_ord_Memrel,
                         ordertype_pred_Inl_eq, 
                         lt_pred_Memrel, leI RS le_ordertype_Memrel]
@@ -424,7 +424,7 @@
 goal OrderType.thy
     "!!A B. A<=B ==> id(A) : ord_iso(A, Memrel(A), A, Memrel(B))";
 by (resolve_tac [id_bij RS ord_isoI] 1);
-by (asm_simp_tac (!simpset addsimps [id_conv, Memrel_iff]) 1);
+by (asm_simp_tac (simpset() addsimps [id_conv, Memrel_iff]) 1);
 by (Blast_tac 1);
 qed "id_ord_iso_Memrel";
 
@@ -445,7 +445,7 @@
 by (rtac RepFun_eqI 1);
 by (etac InrI 2);
 by (asm_simp_tac 
-    (!simpset addsimps [ordertype_pred_Inr_eq, well_ord_Memrel, 
+    (simpset() addsimps [ordertype_pred_Inr_eq, well_ord_Memrel, 
                      lt_pred_Memrel, leI RS le_ordertype_Memrel,
                      ordertype_sum_Memrel]) 1);
 qed "oadd_lt_mono2";
@@ -455,12 +455,12 @@
 by (rtac Ord_linear_lt 1);
 by (REPEAT_SOME assume_tac);
 by (ALLGOALS
-    (blast_tac (!claset addDs [oadd_lt_mono2] addEs [lt_irrefl, lt_asym])));
+    (blast_tac (claset() addDs [oadd_lt_mono2] addEs [lt_irrefl, lt_asym])));
 qed "oadd_lt_cancel2";
 
 goal OrderType.thy
     "!!i j k. [| Ord(i); Ord(j); Ord(k) |] ==> i++j < i++k <-> j<k";
-by (blast_tac (!claset addSIs [oadd_lt_mono2] addSDs [oadd_lt_cancel2]) 1);
+by (blast_tac (claset() addSIs [oadd_lt_mono2] addSDs [oadd_lt_cancel2]) 1);
 qed "oadd_lt_iff2";
 
 goal OrderType.thy
@@ -468,8 +468,8 @@
 by (rtac Ord_linear_lt 1);
 by (REPEAT_SOME assume_tac);
 by (ALLGOALS
-    (fast_tac (!claset addDs [oadd_lt_mono2] 
-                       addss (!simpset addsimps [lt_not_refl]))));
+    (fast_tac (claset() addDs [oadd_lt_mono2] 
+                       addss (simpset() addsimps [lt_not_refl]))));
 qed "oadd_inject";
 
 goalw OrderType.thy [oadd_def] 
@@ -477,11 +477,11 @@
 (*Rotate the hypotheses so that simplification will work*)
 by (etac revcut_rl 1);
 by (asm_full_simp_tac 
-    (!simpset addsimps [ordertype_pred_unfold, well_ord_radd,
+    (simpset() addsimps [ordertype_pred_unfold, well_ord_radd,
                      well_ord_Memrel]) 1);
 by (eresolve_tac [ltD RS RepFunE] 1);
-by (fast_tac (!claset addss 
-              (!simpset addsimps [ordertype_pred_Inl_eq, well_ord_Memrel, 
+by (fast_tac (claset() addss 
+              (simpset() addsimps [ordertype_pred_Inl_eq, well_ord_Memrel, 
                                ltI, lt_pred_Memrel, le_ordertype_Memrel, leI,
                                ordertype_pred_Inr_eq, 
                                ordertype_sum_Memrel])) 1);
@@ -507,14 +507,14 @@
 by (rtac (subsetI RS equalityI) 1);
 by (eresolve_tac [ltI RS lt_oadd_disj RS disjE] 1);
 by (REPEAT (ares_tac [Ord_oadd] 1));
-by (fast_tac (!claset addIs [lt_oadd1, oadd_lt_mono2]
-                      addss (!simpset addsimps [Ord_mem_iff_lt, Ord_oadd])) 3);
+by (fast_tac (claset() addIs [lt_oadd1, oadd_lt_mono2]
+                      addss (simpset() addsimps [Ord_mem_iff_lt, Ord_oadd])) 3);
 by (Blast_tac 2);
-by (blast_tac (!claset addSEs [ltE]) 1);
+by (blast_tac (claset() addSEs [ltE]) 1);
 qed "oadd_unfold";
 
 goal OrderType.thy "!!i. Ord(i) ==> i++1 = succ(i)";
-by (asm_simp_tac (!simpset addsimps [oadd_unfold, Ord_1, oadd_0]) 1);
+by (asm_simp_tac (simpset() addsimps [oadd_unfold, Ord_1, oadd_0]) 1);
 by (Blast_tac 1);
 qed "oadd_1";
 
@@ -522,7 +522,7 @@
     "!!i. [| Ord(i);  Ord(j) |] ==> i++succ(j) = succ(i++j)";
                 (*ZF_ss prevents looping*)
 by (asm_simp_tac (ZF_ss addsimps [Ord_oadd, oadd_1 RS sym]) 1);
-by (asm_simp_tac (!simpset addsimps [oadd_1, oadd_assoc, Ord_1]) 1);
+by (asm_simp_tac (simpset() addsimps [oadd_1, oadd_assoc, Ord_1]) 1);
 qed "oadd_succ";
 
 
@@ -531,7 +531,7 @@
 val prems = goal OrderType.thy
     "[| Ord(i);  !!x. x:A ==> Ord(j(x));  a:A |] ==> \
 \    i ++ (UN x:A. j(x)) = (UN x:A. i++j(x))";
-by (blast_tac (!claset addIs (prems @ [ltI, Ord_UN, Ord_oadd, 
+by (blast_tac (claset() addIs (prems @ [ltI, Ord_UN, Ord_oadd, 
                                     lt_oadd1 RS ltD, oadd_lt_mono2 RS ltD])
                      addSEs [ltE, ltI RS lt_oadd_disj RS disjE]) 1);
 qed "oadd_UN";
@@ -539,7 +539,7 @@
 goal OrderType.thy 
     "!!i j. [| Ord(i);  Limit(j) |] ==> i++j = (UN k:j. i++k)";
 by (forward_tac [Limit_has_0 RS ltD] 1);
-by (asm_simp_tac (!simpset addsimps [Limit_is_Ord RS Ord_in_Ord,
+by (asm_simp_tac (simpset() addsimps [Limit_is_Ord RS Ord_in_Ord,
                                   oadd_UN RS sym, Union_eq_UN RS sym, 
                                   Limit_Union_eq]) 1);
 qed "oadd_Limit";
@@ -548,13 +548,13 @@
 
 goal OrderType.thy "!!i j. [| Ord(i);  Ord(j) |] ==> i le j++i";
 by (eres_inst_tac [("i","i")] trans_induct3 1);
-by (asm_simp_tac (!simpset addsimps [Ord_0_le]) 1);
-by (asm_simp_tac (!simpset addsimps [oadd_succ, succ_leI]) 1);
-by (asm_simp_tac (!simpset addsimps [oadd_Limit]) 1);
+by (asm_simp_tac (simpset() addsimps [Ord_0_le]) 1);
+by (asm_simp_tac (simpset() addsimps [oadd_succ, succ_leI]) 1);
+by (asm_simp_tac (simpset() addsimps [oadd_Limit]) 1);
 by (rtac le_trans 1);
 by (rtac le_implies_UN_le_UN 2);
 by (Blast_tac 2);
-by (asm_simp_tac (!simpset addsimps [Union_eq_UN RS sym, Limit_Union_eq, 
+by (asm_simp_tac (simpset() addsimps [Union_eq_UN RS sym, Limit_Union_eq, 
                                      le_refl, Limit_is_Ord]) 1);
 qed "oadd_le_self2";
 
@@ -563,8 +563,8 @@
 by (forward_tac [le_Ord2] 1);
 by (etac trans_induct3 1);
 by (Asm_simp_tac 1);
-by (asm_simp_tac (!simpset addsimps [oadd_succ, succ_le_iff]) 1);
-by (asm_simp_tac (!simpset addsimps [oadd_Limit]) 1);
+by (asm_simp_tac (simpset() addsimps [oadd_succ, succ_le_iff]) 1);
+by (asm_simp_tac (simpset() addsimps [oadd_Limit]) 1);
 by (rtac le_implies_UN_le_UN 1);
 by (Blast_tac 1);
 qed "oadd_le_mono1";
@@ -576,12 +576,12 @@
 qed "oadd_lt_mono";
 
 goal OrderType.thy "!!i j. [| i' le i;  j' le j |] ==> i'++j' le i++j";
-by (asm_simp_tac (!simpset addsimps [oadd_succ RS sym, le_Ord2, oadd_lt_mono]) 1);
+by (asm_simp_tac (simpset() addsimps [oadd_succ RS sym, le_Ord2, oadd_lt_mono]) 1);
 qed "oadd_le_mono";
 
 goal OrderType.thy
     "!!i j k. [| Ord(i); Ord(j); Ord(k) |] ==> i++j le i++k <-> j le k";
-by (asm_simp_tac (!simpset addsimps [oadd_lt_iff2, oadd_succ RS sym, 
+by (asm_simp_tac (simpset() addsimps [oadd_lt_iff2, oadd_succ RS sym, 
                                   Ord_succ]) 1);
 qed "oadd_le_iff2";
 
@@ -593,32 +593,32 @@
 goal OrderType.thy
     "!!A B. A<=B ==> (lam y:B. if(y:A, Inl(y), Inr(y))) : bij(B, A+(B-A))";
 by (res_inst_tac [("d", "case(%x. x, %y. y)")] lam_bijective 1);
-by (blast_tac (!claset addSIs [if_type]) 1);
-by (fast_tac (!claset addSIs [case_type]) 1);
+by (blast_tac (claset() addSIs [if_type]) 1);
+by (fast_tac (claset() addSIs [case_type]) 1);
 by (etac sumE 2);
-by (ALLGOALS (asm_simp_tac (!simpset setloop split_tac [expand_if])));
+by (ALLGOALS (asm_simp_tac (simpset() setloop split_tac [expand_if])));
 qed "bij_sum_Diff";
 
 goal OrderType.thy
     "!!i j. i le j ==>  \
 \           ordertype(i+(j-i), radd(i,Memrel(j),j-i,Memrel(j))) =       \
 \           ordertype(j, Memrel(j))";
-by (safe_tac (!claset addSDs [le_subset_iff RS iffD1]));
+by (safe_tac (claset() addSDs [le_subset_iff RS iffD1]));
 by (resolve_tac [bij_sum_Diff RS ord_isoI RS ord_iso_sym RS ordertype_eq] 1);
 by (etac well_ord_Memrel 3);
 by (assume_tac 1);
 by (asm_simp_tac 
-     (!simpset setloop split_tac [expand_if] addsimps [Memrel_iff]) 1);
+     (simpset() setloop split_tac [expand_if] addsimps [Memrel_iff]) 1);
 by (forw_inst_tac [("j", "y")] Ord_in_Ord 1 THEN assume_tac 1);
 by (forw_inst_tac [("j", "x")] Ord_in_Ord 1 THEN assume_tac 1);
-by (asm_simp_tac (!simpset addsimps [Ord_mem_iff_lt, lt_Ord, not_lt_iff_le]) 1);
-by (blast_tac (!claset addIs [lt_trans2, lt_trans]) 1);
+by (asm_simp_tac (simpset() addsimps [Ord_mem_iff_lt, lt_Ord, not_lt_iff_le]) 1);
+by (blast_tac (claset() addIs [lt_trans2, lt_trans]) 1);
 qed "ordertype_sum_Diff";
 
 goalw OrderType.thy [oadd_def, odiff_def]
     "!!i j. i le j ==>  \
 \           i ++ (j--i) = ordertype(i+(j-i), radd(i,Memrel(j),j-i,Memrel(j)))";
-by (safe_tac (!claset addSDs [le_subset_iff RS iffD1]));
+by (safe_tac (claset() addSDs [le_subset_iff RS iffD1]));
 by (resolve_tac [sum_ord_iso_cong RS ordertype_eq] 1);
 by (etac id_ord_iso_Memrel 1);
 by (resolve_tac [ordertype_ord_iso RS ord_iso_sym] 1);
@@ -627,7 +627,7 @@
 qed "oadd_ordertype_Diff";
 
 goal OrderType.thy "!!i j. i le j ==> i ++ (j--i) = j";
-by (asm_simp_tac (!simpset addsimps [oadd_ordertype_Diff, ordertype_sum_Diff, 
+by (asm_simp_tac (simpset() addsimps [oadd_ordertype_Diff, ordertype_sum_Diff, 
                                   ordertype_Memrel, lt_Ord2 RS Ord_succD]) 1);
 qed "oadd_odiff_inverse";
 
@@ -643,14 +643,14 @@
     "!!i j. [| Ord(i); Ord(j) |] ==> (i++j) -- i = j";
 by (rtac oadd_inject 1);
 by (REPEAT (ares_tac [Ord_ordertype, Ord_oadd, Ord_odiff] 2));
-by (asm_simp_tac (!simpset addsimps [oadd_odiff_inverse, oadd_le_self]) 1);
+by (asm_simp_tac (simpset() addsimps [oadd_odiff_inverse, oadd_le_self]) 1);
 qed "odiff_oadd_inverse";
 
 val [i_lt_j, k_le_i] = goal OrderType.thy
     "[| i<j;  k le i |] ==> i--k < j--k";
 by (rtac (k_le_i RS lt_Ord RSN (2,oadd_lt_cancel2)) 1);
 by (simp_tac
-    (!simpset addsimps [i_lt_j, k_le_i, [k_le_i, leI] MRS le_trans,
+    (simpset() addsimps [i_lt_j, k_le_i, [k_le_i, leI] MRS le_trans,
                      oadd_odiff_inverse]) 1);
 by (REPEAT (resolve_tac (Ord_odiff :: 
                          ([i_lt_j, k_le_i] RL [lt_Ord, lt_Ord2])) 1));
@@ -671,8 +671,8 @@
 \        pred(A*B, <a,b>, rmult(A,r,B,s)) =     \
 \        pred(A,a,r)*B Un ({a} * pred(B,b,s))";
 by (rtac equalityI 1);
-by (safe_tac (!claset));
-by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [rmult_iff])));
+by (safe_tac (claset()));
+by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [rmult_iff])));
 by (ALLGOALS (Blast_tac));
 qed "pred_Pair_eq";
 
@@ -681,11 +681,11 @@
 \        ordertype(pred(A*B, <a,b>, rmult(A,r,B,s)), rmult(A,r,B,s)) = \
 \        ordertype(pred(A,a,r)*B + pred(B,b,s),                        \
 \                 radd(A*B, rmult(A,r,B,s), B, s))";
-by (asm_simp_tac (!simpset addsimps [pred_Pair_eq]) 1);
+by (asm_simp_tac (simpset() addsimps [pred_Pair_eq]) 1);
 by (resolve_tac [ordertype_eq RS sym] 1);
 by (rtac prod_sum_singleton_ord_iso 1);
 by (REPEAT_FIRST (ares_tac [pred_subset, well_ord_rmult RS well_ord_subset]));
-by (blast_tac (!claset addSEs [predE]) 1);
+by (blast_tac (claset() addSEs [predE]) 1);
 qed "ordertype_pred_Pair_eq";
 
 goalw OrderType.thy [oadd_def, omult_def]
@@ -693,7 +693,7 @@
 \        ordertype(pred(i*j, <i',j'>, rmult(i,Memrel(i),j,Memrel(j))), \
 \                  rmult(i,Memrel(i),j,Memrel(j))) =                   \
 \        j**i' ++ j'";
-by (asm_simp_tac (!simpset addsimps [ordertype_pred_Pair_eq, lt_pred_Memrel, 
+by (asm_simp_tac (simpset() addsimps [ordertype_pred_Pair_eq, lt_pred_Memrel, 
 				     ltD, lt_Ord2, well_ord_Memrel]) 1);
 by (rtac trans 1);
 by (resolve_tac [ordertype_ord_iso RS sum_ord_iso_cong RS ordertype_eq] 2);
@@ -702,35 +702,35 @@
 by (REPEAT_FIRST (eresolve_tac [SigmaE, sumE, ltE, ssubst]));
 by (REPEAT_FIRST (ares_tac [well_ord_rmult, well_ord_radd, well_ord_Memrel, 
                             Ord_ordertype]));
-by (ALLGOALS (asm_simp_tac (!simpset addsimps [Memrel_iff])));
-by (safe_tac (!claset));
-by (ALLGOALS (blast_tac (!claset addIs [Ord_trans])));
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [Memrel_iff])));
+by (safe_tac (claset()));
+by (ALLGOALS (blast_tac (claset() addIs [Ord_trans])));
 qed "ordertype_pred_Pair_lemma";
 
 goalw OrderType.thy [omult_def]
  "!!i j. [| Ord(i);  Ord(j);  k<j**i |] ==>  \
 \        EX j' i'. k = j**i' ++ j' & j'<j & i'<i";
-by (asm_full_simp_tac (!simpset addsimps [ordertype_pred_unfold, 
+by (asm_full_simp_tac (simpset() addsimps [ordertype_pred_unfold, 
                                        well_ord_rmult, well_ord_Memrel]) 1);
-by (safe_tac (!claset addSEs [ltE]));
-by (asm_simp_tac (!simpset addsimps [ordertype_pred_Pair_lemma, ltI,
+by (safe_tac (claset() addSEs [ltE]));
+by (asm_simp_tac (simpset() addsimps [ordertype_pred_Pair_lemma, ltI,
 				     symmetric omult_def]) 1);
-by (blast_tac (!claset addIs [ltI]) 1);
+by (blast_tac (claset() addIs [ltI]) 1);
 qed "lt_omult";
 
 goalw OrderType.thy [omult_def]
  "!!i j. [| j'<j;  i'<i |] ==> j**i' ++ j'  <  j**i";
 by (rtac ltI 1);
 by (asm_simp_tac
-    (!simpset addsimps [Ord_ordertype, well_ord_rmult, well_ord_Memrel, 
+    (simpset() addsimps [Ord_ordertype, well_ord_rmult, well_ord_Memrel, 
                         lt_Ord2]) 2);
 by (asm_simp_tac 
-    (!simpset addsimps [ordertype_pred_unfold, 
+    (simpset() addsimps [ordertype_pred_unfold, 
                      well_ord_rmult, well_ord_Memrel, lt_Ord2]) 1);
 by (rtac bexI 1);
-by (blast_tac (!claset addSEs [ltE]) 2);
+by (blast_tac (claset() addSEs [ltE]) 2);
 by (asm_simp_tac 
-    (!simpset addsimps [ordertype_pred_Pair_lemma, ltI,
+    (simpset() addsimps [ordertype_pred_Pair_lemma, ltI,
                         symmetric omult_def]) 1);
 qed "omult_oadd_lt";
 
@@ -740,8 +740,8 @@
 by (resolve_tac [lt_omult RS exE] 1);
 by (etac ltI 3);
 by (REPEAT (ares_tac [Ord_omult] 1));
-by (blast_tac (!claset addSEs [ltE]) 1);
-by (blast_tac (!claset addIs [omult_oadd_lt RS ltD, ltI]) 1);
+by (blast_tac (claset() addSEs [ltE]) 1);
+by (blast_tac (claset() addIs [omult_oadd_lt RS ltD, ltI]) 1);
 qed "omult_unfold";
 
 (*** Basic laws for ordinal multiplication ***)
@@ -765,7 +765,7 @@
 by (res_inst_tac [("c", "snd"), ("d", "%z.<0,z>")] lam_bijective 1);
 by (REPEAT_FIRST (eresolve_tac [snd_type, SigmaE, succE, emptyE, 
                                 well_ord_Memrel, ordertype_Memrel]));
-by (ALLGOALS (asm_simp_tac (!simpset addsimps [rmult_iff, Memrel_iff])));
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [rmult_iff, Memrel_iff])));
 qed "omult_1";
 
 goalw OrderType.thy [omult_def] "!!i. Ord(i) ==> 1**i = i";
@@ -773,7 +773,7 @@
 by (res_inst_tac [("c", "fst"), ("d", "%z.<z,0>")] lam_bijective 1);
 by (REPEAT_FIRST (eresolve_tac [fst_type, SigmaE, succE, emptyE, 
                                 well_ord_Memrel, ordertype_Memrel]));
-by (ALLGOALS (asm_simp_tac (!simpset addsimps [rmult_iff, Memrel_iff])));
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [rmult_iff, Memrel_iff])));
 qed "omult_1_left";
 
 Addsimps [omult_1, omult_1_left];
@@ -798,7 +798,7 @@
                 (*ZF_ss prevents looping*)
 by (asm_simp_tac (ZF_ss addsimps [oadd_1 RS sym]) 1);
 by (asm_simp_tac 
-    (!simpset addsimps [omult_1, oadd_omult_distrib, Ord_1]) 1);
+    (simpset() addsimps [omult_1, oadd_omult_distrib, Ord_1]) 1);
 qed "omult_succ";
 
 (** Associative law **)
@@ -822,14 +822,14 @@
 val prems = goal OrderType.thy
     "[| Ord(i);  !!x. x:A ==> Ord(j(x)) |] ==> \
 \    i ** (UN x:A. j(x)) = (UN x:A. i**j(x))";
-by (asm_simp_tac (!simpset addsimps (prems@[Ord_UN, omult_unfold])) 1);
+by (asm_simp_tac (simpset() addsimps (prems@[Ord_UN, omult_unfold])) 1);
 by (Blast_tac 1);
 qed "omult_UN";
 
 goal OrderType.thy 
     "!!i j. [| Ord(i);  Limit(j) |] ==> i**j = (UN k:j. i**k)";
 by (asm_simp_tac 
-    (!simpset addsimps [Limit_is_Ord RS Ord_in_Ord, omult_UN RS sym, 
+    (simpset() addsimps [Limit_is_Ord RS Ord_in_Ord, omult_UN RS sym, 
                      Union_eq_UN RS sym, Limit_Union_eq]) 1);
 qed "omult_Limit";
 
@@ -838,8 +838,8 @@
 
 (*As a special case we have "[| 0<i;  0<j |] ==> 0 < i**j" *)
 goal OrderType.thy "!!i j. [| k<i;  0<j |] ==> k < i**j";
-by (safe_tac (!claset addSEs [ltE] addSIs [ltI, Ord_omult]));
-by (asm_simp_tac (!simpset addsimps [omult_unfold]) 1);
+by (safe_tac (claset() addSEs [ltE] addSIs [ltI, Ord_omult]));
+by (asm_simp_tac (simpset() addsimps [omult_unfold]) 1);
 by (REPEAT_FIRST (ares_tac [bexI]));
 by (Asm_simp_tac 1);
 qed "lt_omult1";
@@ -853,26 +853,26 @@
 by (forward_tac [lt_Ord] 1);
 by (forward_tac [le_Ord2] 1);
 by (etac trans_induct3 1);
-by (asm_simp_tac (!simpset addsimps [le_refl, Ord_0]) 1);
-by (asm_simp_tac (!simpset addsimps [omult_succ, oadd_le_mono]) 1);
-by (asm_simp_tac (!simpset addsimps [omult_Limit]) 1);
+by (asm_simp_tac (simpset() addsimps [le_refl, Ord_0]) 1);
+by (asm_simp_tac (simpset() addsimps [omult_succ, oadd_le_mono]) 1);
+by (asm_simp_tac (simpset() addsimps [omult_Limit]) 1);
 by (rtac le_implies_UN_le_UN 1);
 by (Blast_tac 1);
 qed "omult_le_mono1";
 
 goal OrderType.thy "!!i j k. [| k<j;  0<i |] ==> i**k < i**j";
 by (rtac ltI 1);
-by (asm_simp_tac (!simpset addsimps [omult_unfold, lt_Ord2]) 1);
-by (safe_tac (!claset addSEs [ltE] addSIs [Ord_omult]));
+by (asm_simp_tac (simpset() addsimps [omult_unfold, lt_Ord2]) 1);
+by (safe_tac (claset() addSEs [ltE] addSIs [Ord_omult]));
 by (REPEAT_FIRST (ares_tac [bexI]));
-by (asm_simp_tac (!simpset addsimps [Ord_omult]) 1);
+by (asm_simp_tac (simpset() addsimps [Ord_omult]) 1);
 qed "omult_lt_mono2";
 
 goal OrderType.thy "!!i j k. [| k le j;  Ord(i) |] ==> i**k le i**j";
 by (rtac subset_imp_le 1);
-by (safe_tac (!claset addSEs [ltE, make_elim Ord_succD] addSIs [Ord_omult]));
-by (asm_full_simp_tac (!simpset addsimps [omult_unfold]) 1);
-by (deepen_tac (!claset addEs [Ord_trans]) 0 1);
+by (safe_tac (claset() addSEs [ltE, make_elim Ord_succD] addSIs [Ord_omult]));
+by (asm_full_simp_tac (simpset() addsimps [omult_unfold]) 1);
+by (deepen_tac (claset() addEs [Ord_trans]) 0 1);
 qed "omult_le_mono2";
 
 goal OrderType.thy "!!i j. [| i' le i;  j' le j |] ==> i'**j' le i**j";
@@ -891,17 +891,17 @@
 goal OrderType.thy "!!i j. [| Ord(i);  0<j |] ==> i le j**i";
 by (forward_tac [lt_Ord2] 1);
 by (eres_inst_tac [("i","i")] trans_induct3 1);
-by (asm_simp_tac (!simpset addsimps [omult_0, Ord_0 RS le_refl]) 1);
-by (asm_simp_tac (!simpset addsimps [omult_succ, succ_le_iff]) 1);
+by (asm_simp_tac (simpset() addsimps [omult_0, Ord_0 RS le_refl]) 1);
+by (asm_simp_tac (simpset() addsimps [omult_succ, succ_le_iff]) 1);
 by (etac lt_trans1 1);
 by (res_inst_tac [("b", "j**x")] (oadd_0 RS subst) 1 THEN 
     rtac oadd_lt_mono2 2);
 by (REPEAT (ares_tac [Ord_omult] 1));
-by (asm_simp_tac (!simpset addsimps [omult_Limit]) 1);
+by (asm_simp_tac (simpset() addsimps [omult_Limit]) 1);
 by (rtac le_trans 1);
 by (rtac le_implies_UN_le_UN 2);
 by (Blast_tac 2);
-by (asm_simp_tac (!simpset addsimps [Union_eq_UN RS sym, Limit_Union_eq, 
+by (asm_simp_tac (simpset() addsimps [Union_eq_UN RS sym, Limit_Union_eq, 
                                      Limit_is_Ord RS le_refl]) 1);
 qed "omult_le_self2";
 
@@ -912,8 +912,8 @@
 by (rtac Ord_linear_lt 1);
 by (REPEAT_SOME assume_tac);
 by (ALLGOALS
-    (best_tac (!claset addDs [omult_lt_mono2] 
-                       addss (!simpset addsimps [lt_not_refl]))));
+    (best_tac (claset() addDs [omult_lt_mono2] 
+                       addss (simpset() addsimps [lt_not_refl]))));
 qed "omult_inject";