src/HOL/Isar_examples/Summation.thy
changeset 8910 981ac87f905c
parent 8814 0a5edcbe0695
child 9659 b9cf6801f3da