src/ZF/Univ.ML

 
 goal Univ.thy "Vfrom(A,x) <= Vfrom(A,rank(x))";
 by (eps_ind_tac "x" 1);
 by (stac Vfrom 1);
 by (stac Vfrom 1);
-by (blast_tac (!claset addSIs [rank_lt RS ltD]) 1);
+by (blast_tac (claset() addSIs [rank_lt RS ltD]) 1);
 qed "Vfrom_rank_subset1";
 
 goal Univ.thy "Vfrom(A,rank(x)) <= Vfrom(A,x)";
 by (eps_ind_tac "x" 1);
 by (stac Vfrom 1);

 
 (** Finite sets and ordered pairs **)
 
 goal Univ.thy "!!a. a: Vfrom(A,i) ==> {a} : Vfrom(A,succ(i))";
 by (rtac subset_mem_Vfrom 1);
-by (safe_tac (!claset));
+by (safe_tac (claset()));
 qed "singleton_in_Vfrom";
 
 goal Univ.thy
     "!!A. [| a: Vfrom(A,i);  b: Vfrom(A,i) |] ==> {a,b} : Vfrom(A,succ(i))";
 by (rtac subset_mem_Vfrom 1);
-by (safe_tac (!claset));
+by (safe_tac (claset()));
 qed "doubleton_in_Vfrom";
 
 goalw Univ.thy [Pair_def]
     "!!A. [| a: Vfrom(A,i);  b: Vfrom(A,i) |] ==> \
 \         <a,b> : Vfrom(A,succ(succ(i)))";

     "!!A b. [| b: Vfrom(A,i); Limit(i) |] ==> Inr(b) : Vfrom(A,i)";
 by (REPEAT (ares_tac [one_in_VLimit, Pair_in_VLimit] 1));
 qed "Inr_in_VLimit";
 
 goal Univ.thy "!!i. Limit(i) ==> Vfrom(C,i)+Vfrom(C,i) <= Vfrom(C,i)";
-by (blast_tac (!claset addSIs [Inl_in_VLimit, Inr_in_VLimit]) 1);
+by (blast_tac (claset() addSIs [Inl_in_VLimit, Inr_in_VLimit]) 1);
 qed "sum_VLimit";
 
 bind_thm ("sum_subset_VLimit", [sum_mono, sum_VLimit] MRS subset_trans);
 
 

 (*** Properties assuming Transset(A) ***)
 
 goal Univ.thy "!!i A. Transset(A) ==> Transset(Vfrom(A,i))";
 by (eps_ind_tac "i" 1);
 by (stac Vfrom 1);
-by (blast_tac (!claset addSIs [Transset_Union_family, Transset_Un,
+by (blast_tac (claset() addSIs [Transset_Union_family, Transset_Un,
                             Transset_Pow]) 1);
 qed "Transset_Vfrom";
 
 goal Univ.thy "!!A i. Transset(A) ==> Vfrom(A, succ(i)) = Pow(Vfrom(A,i))";
 by (rtac (Vfrom_succ RS trans) 1);

     "!!A. [| a: Vfrom(A,j);  b: Vfrom(A,j);  Transset(A) |] ==> \
 \         a*b : Vfrom(A, succ(succ(succ(j))))";
 by (dtac Transset_Vfrom 1);
 by (rtac subset_mem_Vfrom 1);
 by (rewtac Transset_def);
-by (blast_tac (!claset addIs [Pair_in_Vfrom]) 1);
+by (blast_tac (claset() addIs [Pair_in_Vfrom]) 1);
 qed "prod_in_Vfrom";
 
 val [aprem,bprem,limiti,transset] = goal Univ.thy
   "[| a: Vfrom(A,i);  b: Vfrom(A,i);  Limit(i);  Transset(A) |] ==> \
 \  a*b : Vfrom(A,i)";

     "!!A. [| a: Vfrom(A,j);  b: Vfrom(A,j);  Transset(A);  1:j |] ==> \
 \         a+b : Vfrom(A, succ(succ(succ(j))))";
 by (dtac Transset_Vfrom 1);
 by (rtac subset_mem_Vfrom 1);
 by (rewtac Transset_def);
-by (blast_tac (!claset addIs [zero_in_Vfrom, Pair_in_Vfrom, 
+by (blast_tac (claset() addIs [zero_in_Vfrom, Pair_in_Vfrom, 
                            i_subset_Vfrom RS subsetD]) 1);
 qed "sum_in_Vfrom";
 
 val [aprem,bprem,limiti,transset] = goal Univ.thy
   "[| a: Vfrom(A,i);  b: Vfrom(A,i);  Limit(i);  Transset(A) |] ==> \

 by (rtac (subset_trans RS subset_trans) 1);
 by (rtac Un_upper2 3);
 by (rtac (succI1 RS UN_upper) 2);
 by (rtac Pow_mono 1);
 by (rewtac Transset_def);
-by (blast_tac (!claset addIs [Pair_in_Vfrom]) 1);
+by (blast_tac (claset() addIs [Pair_in_Vfrom]) 1);
 qed "fun_in_Vfrom";
 
 val [aprem,bprem,limiti,transset] = goal Univ.thy
   "[| a: Vfrom(A,i);  b: Vfrom(A,i);  Limit(i);  Transset(A) |] ==> \
 \  a->b : Vfrom(A,i)";

 by (Blast_tac 1);
 qed "Pow_in_Vfrom";
 
 goal Univ.thy
   "!!a. [| a: Vfrom(A,i);  Limit(i);  Transset(A) |] ==> Pow(a) : Vfrom(A,i)";
-by (blast_tac (!claset addEs [Limit_VfromE]
+by (blast_tac (claset() addEs [Limit_VfromE]
 		       addIs [Limit_has_succ, Pow_in_Vfrom, Limit_VfromI]) 1);
 qed "Pow_in_VLimit";
 
 
 (*** The set Vset(i) ***)

 (** Characterisation of the elements of Vset(i) **)
 
 val [ordi] = goal Univ.thy "Ord(i) ==> ALL b. b : Vset(i) --> rank(b) < i";
 by (rtac (ordi RS trans_induct) 1);
 by (stac Vset 1);
-by (safe_tac (!claset));
+by (safe_tac (claset()));
 by (stac rank 1);
 by (rtac UN_succ_least_lt 1);
 by (Blast_tac 2);
 by (REPEAT (ares_tac [ltI] 1));
 qed_spec_mp "VsetD";
 
 val [ordi] = goal Univ.thy "Ord(i) ==> ALL b. rank(b) : i --> b : Vset(i)";
 by (rtac (ordi RS trans_induct) 1);
 by (rtac allI 1);
 by (stac Vset 1);
-by (blast_tac (!claset addSIs [rank_lt RS ltD]) 1);
+by (blast_tac (claset() addSIs [rank_lt RS ltD]) 1);
 val lemma = result();
 
 goal Univ.thy "!!x i. rank(x)<i ==> x : Vset(i)";
 by (etac ltE 1);
 by (etac (lemma RS spec RS mp) 1);

 qed "Vset_rank_iff";
 
 goal Univ.thy "!!i. Ord(i) ==> rank(Vset(i)) = i";
 by (stac rank 1);
 by (rtac equalityI 1);
-by (safe_tac (!claset));
+by (safe_tac (claset()));
 by (EVERY' [rtac UN_I, 
             etac (i_subset_Vfrom RS subsetD),
             etac (Ord_in_Ord RS rank_of_Ord RS ssubst),
             assume_tac,
             rtac succI1] 3);

 qed "rank_Inr";
 
 val rank_rls = [rank_Inl, rank_Inr, rank_pair1, rank_pair2];
 val rank_trans_rls = rank_rls @ (rank_rls RLN (2, [lt_trans]));
 
-val rank_ss = !simpset addsimps [VsetI] addsimps rank_trans_rls;
+val rank_ss = simpset() addsimps [VsetI] addsimps rank_trans_rls;
 
 (** Recursion over Vset levels! **)
 
 (*NOT SUITABLE FOR REWRITING: recursive!*)
 goalw Univ.thy [Vrec_def] "Vrec(a,H) = H(a, lam x:Vset(rank(a)). Vrec(x,H))";
 by (stac transrec 1);
-by (simp_tac (!simpset addsimps [Ord_rank, Ord_succ, VsetD RS ltD RS beta, 
+by (simp_tac (simpset() addsimps [Ord_rank, Ord_succ, VsetD RS ltD RS beta, 
                               VsetI RS beta, le_refl]) 1);
 qed "Vrec";
 
 (*This form avoids giant explosions in proofs.  NOTE USE OF == *)
 val rew::prems = goal Univ.thy

 goal Univ.thy "2 : univ(A)";
 by (REPEAT (ares_tac [nat_into_univ, nat_0I, nat_succI] 1));
 qed "two_in_univ";
 
 goalw Univ.thy [bool_def] "bool <= univ(A)";
-by (blast_tac (!claset addSIs [zero_in_univ,one_in_univ]) 1);
+by (blast_tac (claset() addSIs [zero_in_univ,one_in_univ]) 1);
 qed "bool_subset_univ";
 
 bind_thm ("bool_into_univ", (bool_subset_univ RS subsetD));
 
 

 (** Closure under finite powerset **)
 
 goal Univ.thy
    "!!i. [| b: Fin(Vfrom(A,i));  Limit(i) |] ==> EX j. b <= Vfrom(A,j) & j<i";
 by (etac Fin_induct 1);
-by (blast_tac (!claset addSDs [Limit_has_0]) 1);
-by (safe_tac (!claset));
+by (blast_tac (claset() addSDs [Limit_has_0]) 1);
+by (safe_tac (claset()));
 by (etac Limit_VfromE 1);
 by (assume_tac 1);
-by (blast_tac (!claset addSIs [Un_least_lt] addIs [Vfrom_UnI1, Vfrom_UnI2]) 1);
+by (blast_tac (claset() addSIs [Un_least_lt] addIs [Vfrom_UnI1, Vfrom_UnI2]) 1);
 val Fin_Vfrom_lemma = result();
 
 goal Univ.thy "!!i. Limit(i) ==> Fin(Vfrom(A,i)) <= Vfrom(A,i)";
 by (rtac subsetI 1);
 by (dtac Fin_Vfrom_lemma 1);
-by (safe_tac (!claset));
+by (safe_tac (claset()));
 by (resolve_tac [Vfrom RS ssubst] 1);
-by (blast_tac (!claset addSDs [ltD]) 1);
+by (blast_tac (claset() addSDs [ltD]) 1);
 val Fin_VLimit = result();
 
 bind_thm ("Fin_subset_VLimit", [Fin_mono, Fin_VLimit] MRS subset_trans);
 
 goalw Univ.thy [univ_def] "Fin(univ(A)) <= univ(A)";