src/HOL/Library/Extended_Nat.thy
2015-11-11 Andreas Lochbihler 2015-11-11 add lemmas for extended nats and reals
2015-10-10 wenzelm 2015-10-10 prefer symbols;
2015-10-09 wenzelm 2015-10-09 discontinued specific HTML syntax;
2015-09-01 wenzelm 2015-09-01 eliminated \<Colon>;
2015-07-06 wenzelm 2015-07-06 tuned proofs;
2015-07-03 hoelzl 2015-07-03 add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
2015-06-17 wenzelm 2015-06-17 isabelle update_cartouches;
2015-03-04 wenzelm 2015-03-04 tuned signature -- prefer qualified names;
2014-12-09 hoelzl 2014-12-09 move topology on enat to Extended_Real, otherwise Jinja_Threads fails
2014-12-08 hoelzl 2014-12-08 instance bool and enat as topologies
2014-11-13 hoelzl 2014-11-13 import general theorems from AFP/Markov_Models
2014-11-02 wenzelm 2014-11-02 modernized header;
2014-09-11 blanchet 2014-09-11 renamed 'rep_datatype' to 'old_rep_datatype' (HOL)
2014-07-05 haftmann 2014-07-05 prefer ac_simps collections over separate name bindings for add and mult
2014-07-04 haftmann 2014-07-04 reduced name variants for assoc and commute on plus and mult
2014-04-28 wenzelm 2014-04-28 tuned;
2013-11-12 hoelzl 2013-11-12 fix document generation for Extended_Nat
2013-11-12 hoelzl 2013-11-12 better support for enat and ereal conversions
2013-11-12 hoelzl 2013-11-12 enat is countable
2013-07-25 haftmann 2013-07-25 factored syntactic type classes for bot and top (by Alessandro Coglio)
2013-04-18 wenzelm 2013-04-18 simplifier uses proper Proof.context instead of historic type simpset;
2013-03-06 huffman 2013-03-06 avoid using Arith_Data.dest_sum in extended-nat simprocs (it treats 'x - y' as 'x + - y', which is not valid for enat)
2013-02-28 wenzelm 2013-02-28 simplified imports;
2013-01-31 hoelzl 2013-01-31 use order topology for extended reals
2012-10-19 webertj 2012-10-19 Renamed {left,right}_distrib to distrib_{right,left}.
2012-10-12 wenzelm 2012-10-12 discontinued obsolete typedef (open) syntax;
2012-03-25 huffman 2012-03-25 merged fork with new numeral representation (see NEWS)
2011-12-20 noschinl 2011-12-20 add simp rules for enat and ereal
2011-12-07 huffman 2011-12-07 add cancellation simprocs for type enat
2011-11-17 huffman 2011-11-17 remove redundant simp rules plus_enat_0
2011-09-12 nipkow 2011-09-12 new fastforce replacing fastsimp - less confusing name
2011-08-02 huffman 2011-08-02 Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
2011-07-26 hoelzl 2011-07-26 enat is a complete_linorder instance
2011-07-19 hoelzl 2011-07-19 rename Fin to enat
2011-07-19 hoelzl 2011-07-19 add ereal to typeclass infinity
2011-07-19 hoelzl 2011-07-19 add nat => enat coercion
2011-07-19 hoelzl 2011-07-19 Introduce infinity type class
2011-07-19 hoelzl 2011-07-19 rename Nat_Infinity (inat) to Extended_Nat (enat)