changeset 7499 | 23e090051cb8 |
parent 6141 | a6922171b396 |
child 9178 | a7ec0fef9860 |
--- a/src/ZF/IMP/Equiv.ML Mon Sep 06 22:12:08 1999 +0200 +++ b/src/ZF/IMP/Equiv.ML Tue Sep 07 10:40:58 1999 +0200 @@ -79,7 +79,7 @@ (* while *) by Safe_tac; by (ALLGOALS Asm_full_simp_tac); -by (EVERY1 [forward_tac [Gamma_bnd_mono], etac induct, atac]); +by (EVERY1 [ftac Gamma_bnd_mono , etac induct, atac]); by (rewtac Gamma_def); by Safe_tac; by (EVERY1 [dtac bspec, atac]);