(* Title: ZF/UNITY/NatPlus.thy ID: $Id$ Author: Sidi O Ehmety, Cambridge University Computer Laboratory Copyright 2001 University of Cambridge More theorems on naturals *) NatPlus = Main + end