src/HOL/Isar_examples/Summation.thy
changeset 9352 416b2ecd97a1
parent 8814 0a5edcbe0695
child 9659 b9cf6801f3da