src/HOL/Library/Extended_Nat.thy
Fri, 12 Oct 2012 18:58:20 +0200 wenzelm discontinued obsolete typedef (open) syntax;
Sun, 25 Mar 2012 20:15:39 +0200 huffman merged fork with new numeral representation (see NEWS)
Tue, 20 Dec 2011 11:40:56 +0100 noschinl add simp rules for enat and ereal
Wed, 07 Dec 2011 10:50:30 +0100 huffman add cancellation simprocs for type enat
Thu, 17 Nov 2011 07:15:30 +0100 huffman remove redundant simp rules plus_enat_0
Mon, 12 Sep 2011 07:55:43 +0200 nipkow new fastforce replacing fastsimp - less confusing name
Tue, 02 Aug 2011 08:28:34 -0700 huffman Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
Tue, 26 Jul 2011 13:50:03 +0200 hoelzl enat is a complete_linorder instance
Tue, 19 Jul 2011 14:38:48 +0200 hoelzl rename Fin to enat
Tue, 19 Jul 2011 14:38:29 +0200 hoelzl add ereal to typeclass infinity
Tue, 19 Jul 2011 14:37:49 +0200 hoelzl add nat => enat coercion
Tue, 19 Jul 2011 14:37:09 +0200 hoelzl Introduce infinity type class
Tue, 19 Jul 2011 14:35:44 +0200 hoelzl rename Nat_Infinity (inat) to Extended_Nat (enat)
less more (0) tip