src/ZF/IMP/Equiv.ML
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]);