src/ZF/Epsilon.ML

 
 val prems = goal Epsilon.thy
     "[| !!x u. [| x:eclose({a});  u: Pi(x,B) |] ==> H(x,u) : B(x)   \
 \    |]  ==> transrec(a,H) : B(a)";
 by (res_inst_tac [("i", "a")] (arg_in_eclose_sing RS eclose_induct) 1);
-by (rtac (transrec RS ssubst) 1);
+by (stac transrec 1);
 by (REPEAT (ares_tac (prems @ [lam_type]) 1 ORELSE etac bspec 1));
 qed "transrec_type";
 
 goal Epsilon.thy "!!i. Ord(i) ==> eclose({i}) <= succ(i)";
 by (etac (Ord_is_Transset RS Transset_succ RS eclose_least) 1);

 
 (*** Rank ***)
 
 (*NOT SUITABLE FOR REWRITING -- RECURSIVE!*)
 goal Epsilon.thy "rank(a) = (UN y:a. succ(rank(y)))";
-by (rtac (rank_def RS def_transrec RS ssubst) 1);
+by (stac (rank_def RS def_transrec) 1);
 by (simp_tac ZF_ss 1);
 qed "rank";
 
 goal Epsilon.thy "Ord(rank(a))";
 by (eps_ind_tac "a" 1);
-by (rtac (rank RS ssubst) 1);
+by (stac rank 1);
 by (rtac (Ord_succ RS Ord_UN) 1);
 by (etac bspec 1);
 by (assume_tac 1);
 qed "Ord_rank";
 
 val [major] = goal Epsilon.thy "Ord(i) ==> rank(i) = i";
 by (rtac (major RS trans_induct) 1);
-by (rtac (rank RS ssubst) 1);
+by (stac rank 1);
 by (asm_simp_tac (ZF_ss addsimps [Ord_equality]) 1);
 qed "rank_of_Ord";
 
 goal Epsilon.thy "!!a b. a:b ==> rank(a) < rank(b)";
 by (res_inst_tac [("a1","b")] (rank RS ssubst) 1);

 by (assume_tac 1);
 qed "eclose_rank_lt";
 
 goal Epsilon.thy "!!a b. a<=b ==> rank(a) le rank(b)";
 by (rtac subset_imp_le 1);
-by (rtac (rank RS ssubst) 1);
-by (rtac (rank RS ssubst) 1);
+by (stac rank 1);
+by (stac rank 1);
 by (etac UN_mono 1);
 by (REPEAT (resolve_tac [subset_refl, Ord_rank] 1));
 qed "rank_mono";
 
 goal Epsilon.thy "rank(Pow(a)) = succ(rank(a))";

 
 goal Epsilon.thy "rank(Union(A)) = (UN x:A. rank(x))";
 by (rtac equalityI 1);
 by (rtac (rank_mono RS le_imp_subset RS UN_least) 2);
 by (etac Union_upper 2);
-by (rtac (rank RS ssubst) 1);
+by (stac rank 1);
 by (rtac UN_least 1);
 by (etac UnionE 1);
 by (rtac subset_trans 1);
 by (etac (RepFunI RS Union_upper) 2);
 by (etac (rank_lt RS succ_leI RS le_imp_subset) 1);