src/HOL/NatArith.thy
changeset 19446 30e1178d7a3b
parent 17688 91d3604ec4b5
child 21238 c46bc715bdfd