src/HOL/Real/PNat.thy
changeset 8742 8a5b3f58b944
parent 7562 8519d5019309
child 8856 435187ffc64e
equal deleted inserted replaced
8741:61bc5ed22b62 8742:8a5b3f58b944