src/HOL/IMPP/Natural.thy
2015-07-18 wenzelm 2015-07-18 prefer tactics with explicit context;
2015-03-25 wenzelm 2015-03-25 prefer local fixes;
2015-02-10 wenzelm 2015-02-10 tuned;
2015-02-10 wenzelm 2015-02-10 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; occasionally clarified use of context;
2014-11-10 wenzelm 2014-11-10 proper context for assume_tac (atac remains as fall-back without context);
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2013-02-28 wenzelm 2013-02-28 tuned proof;
2012-02-14 wenzelm 2012-02-14 eliminated obsolete aliases;
2011-01-16 wenzelm 2011-01-16 tuned headers;
2010-09-06 wenzelm 2010-09-06 more antiquotations;
2008-06-25 wenzelm 2008-06-25 modernized specifications;
2007-08-07 wenzelm 2007-08-07 turned Unify flags into configuration options (global only);
2007-07-11 berghofe 2007-07-11 Adapted to new inductive definition package.
2006-06-07 wenzelm 2006-06-07 removed obsolete ML files;
2005-09-17 wenzelm 2005-09-17 converted to Isar theory format;
2000-01-31 oheimb 2000-01-31 added IMPP to HOL