changeset 5529 | 4a54acae6a15 |
parent 4971 | 09b8945cac07 |
child 5553 | ae42b36a50c2 |
--- a/src/ZF/indrule.ML Tue Sep 22 13:49:22 1998 +0200 +++ b/src/ZF/indrule.ML Tue Sep 22 13:50:57 1998 +0200 @@ -226,7 +226,7 @@ (*some risk of excessive simplification here -- might have to identify the bare minimum set of rewrites*) full_simp_tac - (mut_ss addsimps (conj_simps @ imp_simps @ quant_simps)) 1 + (mut_ss addsimps conj_simps @ imp_simps @ quant_simps) 1 THEN (*unpackage and use "prem" in the corresponding place*) REPEAT (rtac impI 1) THEN