src/HOL/Real/PNat.thy
changeset 10379 93630e0c5ae9
parent 8856 435187ffc64e
child 10834 a7897aebbffc
equal deleted inserted replaced
10378:98c95ebf804f 10379:93630e0c5ae9