| Wed, 13 Feb 2019 11:25:23 +0100 |
nipkow |
added lemma
|
file |
diff |
annotate
|
| Wed, 13 Feb 2019 07:48:42 +0100 |
nipkow |
too agressive
|
file |
diff |
annotate
|
| Wed, 13 Feb 2019 02:13:46 +0100 |
nipkow |
added lemmas
|
file |
diff |
annotate
|
| Fri, 04 Jan 2019 23:22:53 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Thu, 07 Jun 2018 19:36:12 +0200 |
nipkow |
utilize 'flip'
|
file |
diff |
annotate
|
| Thu, 22 Feb 2018 22:58:27 +0000 |
paulson |
type class linordered_nonzero_semiring has new axiom to guarantee characteristic 0
|
file |
diff |
annotate
|
| Sun, 26 Nov 2017 21:08:32 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Mon, 17 Oct 2016 11:46:22 +0200 |
nipkow |
setsum -> sum
|
file |
diff |
annotate
|
| Fri, 19 Feb 2016 13:40:50 +0100 |
hoelzl |
generalize more theorems to support enat and ennreal
|
file |
diff |
annotate
|
| 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.
|
file |
diff |
annotate
|
| Fri, 19 Feb 2016 12:25:57 +0100 |
hoelzl |
remove lattice syntax from countable complete lattice
|
file |
diff |
annotate
|
| Wed, 11 Nov 2015 10:07:27 +0100 |
Andreas Lochbihler |
add lemmas for extended nats and reals
|
file |
diff |
annotate
|
| Sat, 10 Oct 2015 19:22:05 +0200 |
wenzelm |
prefer symbols;
|
file |
diff |
annotate
|
| Fri, 09 Oct 2015 20:26:03 +0200 |
wenzelm |
discontinued specific HTML syntax;
|
file |
diff |
annotate
|
| Tue, 01 Sep 2015 22:32:58 +0200 |
wenzelm |
eliminated \<Colon>;
|
file |
diff |
annotate
|
| Mon, 06 Jul 2015 22:57:34 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Fri, 03 Jul 2015 08:26:34 +0200 |
hoelzl |
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
|
file |
diff |
annotate
|
| Wed, 17 Jun 2015 11:03:05 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| Wed, 04 Mar 2015 19:53:18 +0100 |
wenzelm |
tuned signature -- prefer qualified names;
|
file |
diff |
annotate
|
| Tue, 09 Dec 2014 16:22:40 +0100 |
hoelzl |
move topology on enat to Extended_Real, otherwise Jinja_Threads fails
|
file |
diff |
annotate
|
| Mon, 08 Dec 2014 14:32:11 +0100 |
hoelzl |
instance bool and enat as topologies
|
file |
diff |
annotate
|
| Thu, 13 Nov 2014 17:19:52 +0100 |
hoelzl |
import general theorems from AFP/Markov_Models
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 17:20:45 +0100 |
wenzelm |
modernized header;
|
file |
diff |
annotate
|
| Thu, 11 Sep 2014 18:54:36 +0200 |
blanchet |
renamed 'rep_datatype' to 'old_rep_datatype' (HOL)
|
file |
diff |
annotate
|
| Sat, 05 Jul 2014 11:01:53 +0200 |
haftmann |
prefer ac_simps collections over separate name bindings for add and mult
|
file |
diff |
annotate
|
| Fri, 04 Jul 2014 20:18:47 +0200 |
haftmann |
reduced name variants for assoc and commute on plus and mult
|
file |
diff |
annotate
|
| Mon, 28 Apr 2014 17:50:03 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 12 Nov 2013 20:08:29 +0100 |
hoelzl |
fix document generation for Extended_Nat
|
file |
diff |
annotate
|
| Tue, 12 Nov 2013 19:28:55 +0100 |
hoelzl |
better support for enat and ereal conversions
|
file |
diff |
annotate
|
| Tue, 12 Nov 2013 19:28:55 +0100 |
hoelzl |
enat is countable
|
file |
diff |
annotate
|
| Thu, 25 Jul 2013 08:57:16 +0200 |
haftmann |
factored syntactic type classes for bot and top (by Alessandro Coglio)
|
file |
diff |
annotate
|
| Thu, 18 Apr 2013 17:07:01 +0200 |
wenzelm |
simplifier uses proper Proof.context instead of historic type simpset;
|
file |
diff |
annotate
|
| 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)
|
file |
diff |
annotate
|
| Thu, 28 Feb 2013 12:24:24 +0100 |
wenzelm |
simplified imports;
|
file |
diff |
annotate
|
| Thu, 31 Jan 2013 11:31:30 +0100 |
hoelzl |
use order topology for extended reals
|
file |
diff |
annotate
|
| Fri, 19 Oct 2012 15:12:52 +0200 |
webertj |
Renamed {left,right}_distrib to distrib_{right,left}.
|
file |
diff |
annotate
|
| Fri, 12 Oct 2012 18:58:20 +0200 |
wenzelm |
discontinued obsolete typedef (open) syntax;
|
file |
diff |
annotate
|
| Sun, 25 Mar 2012 20:15:39 +0200 |
huffman |
merged fork with new numeral representation (see NEWS)
|
file |
diff |
annotate
|
| Tue, 20 Dec 2011 11:40:56 +0100 |
noschinl |
add simp rules for enat and ereal
|
file |
diff |
annotate
|
| Wed, 07 Dec 2011 10:50:30 +0100 |
huffman |
add cancellation simprocs for type enat
|
file |
diff |
annotate
|
| Thu, 17 Nov 2011 07:15:30 +0100 |
huffman |
remove redundant simp rules plus_enat_0
|
file |
diff |
annotate
|
| Mon, 12 Sep 2011 07:55:43 +0200 |
nipkow |
new fastforce replacing fastsimp - less confusing name
|
file |
diff |
annotate
|
| Tue, 02 Aug 2011 08:28:34 -0700 |
huffman |
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
|
file |
diff |
annotate
|
| Tue, 26 Jul 2011 13:50:03 +0200 |
hoelzl |
enat is a complete_linorder instance
|
file |
diff |
annotate
|
| Tue, 19 Jul 2011 14:38:48 +0200 |
hoelzl |
rename Fin to enat
|
file |
diff |
annotate
|
| Tue, 19 Jul 2011 14:38:29 +0200 |
hoelzl |
add ereal to typeclass infinity
|
file |
diff |
annotate
|
| Tue, 19 Jul 2011 14:37:49 +0200 |
hoelzl |
add nat => enat coercion
|
file |
diff |
annotate
|
| Tue, 19 Jul 2011 14:37:09 +0200 |
hoelzl |
Introduce infinity type class
|
file |
diff |
annotate
|
| Tue, 19 Jul 2011 14:35:44 +0200 |
hoelzl |
rename Nat_Infinity (inat) to Extended_Nat (enat)
|
file |
diff |
annotate
| base
|