| changeset 15912 | 47aa1a8fcdc9 |
| parent 15561 | 045a07ac35a7 |
| child 18193 | 54419506df9e |
--- a/src/HOL/Isar_examples/Summation.thy Mon May 02 18:59:50 2005 +0200 +++ b/src/HOL/Isar_examples/Summation.thy Mon May 02 19:00:05 2005 +0200 @@ -9,8 +9,6 @@ imports Main begin -declare setsum_op_ivl_Suc [simp] setsum_cl_ivl_Suc [simp] - text_raw {* \footnote{This example is somewhat reminiscent of the \url{http://isabelle.in.tum.de/library/HOL/ex/NatSum.html}, which is