src/HOL/ex/NatSum.thy
changeset 57874 9c361f94b323
parent 54703 499f92dc6e45
child 58770 ae5e9b4f8daf