| changeset 13535 | 007559e981c7 |
| parent 13241 | 0ffc4403f811 |
| child 14046 | 6616e6c53d48 |
--- a/src/ZF/Induct/FoldSet.ML Tue Aug 27 11:09:33 2002 +0200 +++ b/src/ZF/Induct/FoldSet.ML Tue Aug 27 11:09:35 2002 +0200 @@ -301,7 +301,7 @@ by (asm_simp_tac (simpset() addsimps [setsum_def]) 2); by (etac Finite_induct 1); by Auto_tac; -qed "setsum_0"; +qed "setsum_K0"; (*The reversed orientation looks more natural, but LOOPS as a simprule!*) Goal "[| Finite(C); Finite(D) |] \