changeset 1932 | cc9f1ba8f29a |
parent 1461 | 6bcb44e4d6e5 |
child 2469 | b50b8c0eec01 |
--- a/src/ZF/AC/AC10_AC15.ML Wed Aug 21 11:00:04 1996 +0200 +++ b/src/ZF/AC/AC10_AC15.ML Wed Aug 21 11:43:37 1996 +0200 @@ -190,7 +190,7 @@ by (asm_full_simp_tac (AC_ss addsimps [singleton_eqpoll_1 RS eqpoll_imp_lepoll, singletonI RS not_emptyI]) 1); -by (fast_tac (AC_cs addSEs [singletonE, apply_type]) 1); +by (fast_tac (AC_cs addSEs [apply_type]) 1); qed "AC1_AC13"; (* ********************************************************************** *)