| changeset 5265 | 9d1d4c43c76d |
| parent 5147 | 825877190618 |
| child 5268 | 59ef39008514 |
--- a/src/ZF/Zorn.ML Thu Aug 06 10:37:39 1998 +0200 +++ b/src/ZF/Zorn.ML Thu Aug 06 10:38:57 1998 +0200 @@ -261,7 +261,7 @@ by (asm_full_simp_tac (simpset() addsimps [maxchain_def]) 1); by (rename_tac "c" 1); by (res_inst_tac [("x", "Union(c)")] bexI 1); -by (Blast_tac 2); +by (Fast_tac 2); (*Blast_tac: PROOF FAILED*) by Safe_tac; by (rename_tac "z" 1); by (rtac classical 1);