| changeset 8183 | 344888de76c4 |
| parent 8181 | ee74d3843214 |
| child 8201 | a81d18b0a9b1 |
--- a/src/ZF/Finite.ML Wed Feb 02 12:25:29 2000 +0100 +++ b/src/ZF/Finite.ML Wed Feb 02 12:25:54 2000 +0100 @@ -183,8 +183,8 @@ (subset_refl RSN(2, FiniteFun_mono) RS subsetD) 1); by (fast_tac (claset() addDs [FiniteFun_domain_Fin, Fin.dom_subset RS subsetD]) 1); -by (resolve_tac [fun_FiniteFunI] 1); -be FiniteFun_domain_Fin 1; +by (rtac fun_FiniteFunI 1); +by (etac FiniteFun_domain_Fin 1); by (res_inst_tac [("B" , "range(f)")] fun_weaken_type 1); by (ALLGOALS (blast_tac (claset() addDs