src/HOL/ex/Abstract_NAT.thy
2016-04-26 wenzelm 2016-04-26 misc tuning and modernization;
2014-11-22 wenzelm 2014-11-22 misc tuning and modernization;
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2011-08-30 wenzelm 2011-08-30 tuned document;
2008-12-15 ballarin 2008-12-15 More porting to new locales.
2007-07-11 berghofe 2007-07-11 Renamed inductive2 to inductive.
2007-06-05 wenzelm 2007-06-05 tuned comments;
2006-11-17 wenzelm 2006-11-17 more robust syntax for definition/abbreviation/notation;
2006-11-15 wenzelm 2006-11-15 tuned proofs;
2006-11-14 wenzelm 2006-11-14 converted to 'inductive2'; proper localized definitions; added rec examples;
2006-09-26 haftmann 2006-09-26 renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes
2006-09-11 haftmann 2006-09-11 hid succ, pred in Numeral.thy
2006-09-06 haftmann 2006-09-06 got rid of Numeral.bin type
2006-04-08 wenzelm 2006-04-08 refined 'abbreviation';
2006-02-16 wenzelm 2006-02-16 Abstract Natural Numbers with polymorphic recursion.