src/HOL/Library/Extended_Nat.thy
Wed, 13 Feb 2019 07:48:42 +0100 nipkow too agressive
Wed, 13 Feb 2019 02:13:46 +0100 nipkow added lemmas
Fri, 04 Jan 2019 23:22:53 +0100 wenzelm isabelle update -u control_cartouches;
Thu, 07 Jun 2018 19:36:12 +0200 nipkow utilize 'flip'
Thu, 22 Feb 2018 22:58:27 +0000 paulson type class linordered_nonzero_semiring has new axiom to guarantee characteristic 0
Sun, 26 Nov 2017 21:08:32 +0100 wenzelm more symbols;
Mon, 17 Oct 2016 11:46:22 +0200 nipkow setsum -> sum
Fri, 19 Feb 2016 13:40:50 +0100 hoelzl generalize more theorems to support enat and ennreal
Wed, 10 Feb 2016 18:43:19 +0100 hoelzl Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
Fri, 19 Feb 2016 12:25:57 +0100 hoelzl remove lattice syntax from countable complete lattice
Wed, 11 Nov 2015 10:07:27 +0100 Andreas Lochbihler add lemmas for extended nats and reals
Sat, 10 Oct 2015 19:22:05 +0200 wenzelm prefer symbols;
Fri, 09 Oct 2015 20:26:03 +0200 wenzelm discontinued specific HTML syntax;
Tue, 01 Sep 2015 22:32:58 +0200 wenzelm eliminated \<Colon>;
Mon, 06 Jul 2015 22:57:34 +0200 wenzelm tuned proofs;
Fri, 03 Jul 2015 08:26:34 +0200 hoelzl add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
Wed, 17 Jun 2015 11:03:05 +0200 wenzelm isabelle update_cartouches;
Wed, 04 Mar 2015 19:53:18 +0100 wenzelm tuned signature -- prefer qualified names;
Tue, 09 Dec 2014 16:22:40 +0100 hoelzl move topology on enat to Extended_Real, otherwise Jinja_Threads fails
Mon, 08 Dec 2014 14:32:11 +0100 hoelzl instance bool and enat as topologies
Thu, 13 Nov 2014 17:19:52 +0100 hoelzl import general theorems from AFP/Markov_Models
Sun, 02 Nov 2014 17:20:45 +0100 wenzelm modernized header;
Thu, 11 Sep 2014 18:54:36 +0200 blanchet renamed 'rep_datatype' to 'old_rep_datatype' (HOL)
Sat, 05 Jul 2014 11:01:53 +0200 haftmann prefer ac_simps collections over separate name bindings for add and mult
Fri, 04 Jul 2014 20:18:47 +0200 haftmann reduced name variants for assoc and commute on plus and mult
Mon, 28 Apr 2014 17:50:03 +0200 wenzelm tuned;
Tue, 12 Nov 2013 20:08:29 +0100 hoelzl fix document generation for Extended_Nat
Tue, 12 Nov 2013 19:28:55 +0100 hoelzl better support for enat and ereal conversions
Tue, 12 Nov 2013 19:28:55 +0100 hoelzl enat is countable
Thu, 25 Jul 2013 08:57:16 +0200 haftmann factored syntactic type classes for bot and top (by Alessandro Coglio)
Thu, 18 Apr 2013 17:07:01 +0200 wenzelm simplifier uses proper Proof.context instead of historic type simpset;
Wed, 06 Mar 2013 10:44:43 -0800 huffman avoid using Arith_Data.dest_sum in extended-nat simprocs (it treats 'x - y' as 'x + - y', which is not valid for enat)
Thu, 28 Feb 2013 12:24:24 +0100 wenzelm simplified imports;
Thu, 31 Jan 2013 11:31:30 +0100 hoelzl use order topology for extended reals
Fri, 19 Oct 2012 15:12:52 +0200 webertj Renamed {left,right}_distrib to distrib_{right,left}.
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