src/HOL/ex/NatSum.thy
changeset 57978 8f4a332500e4
parent 54703 499f92dc6e45
child 58770 ae5e9b4f8daf