src/HOL/ex/NatSum.ML
changeset 8702 78b7010db847
parent 8493 60c2f892b1d9
child 8770 bfab4d4b7516
equal deleted inserted replaced
8701:d1975e0c99af 8702:78b7010db847