src/HOL/Nat.thy
changeset 22760 6eafeffe801c
parent 22744 5cbe966d67a2
child 22845 5f9138bcb3d7