changeset 1079 | 2f9f2ea26f8f |
parent 804 | 02430d273ebf |
child 1461 | 6bcb44e4d6e5 |
--- a/src/ZF/Zorn.ML Fri Apr 28 15:38:15 1995 +0200 +++ b/src/ZF/Zorn.ML Mon May 01 11:17:41 1995 +0200 @@ -204,8 +204,6 @@ chain_subset_Pow RS subsetD, choice_super]) 1); (*Now, verify that it increases*) -by (rtac allI 1); -by (rtac impI 1); by (asm_simp_tac (ZF_ss addsimps [Pow_iff, subset_refl] setloop split_tac [expand_if]) 1); by (safe_tac ZF_cs);