| #
9447e0f1 |
|
07-Jun-2018 |
nipkow <none@none> |
utilize 'flip'
|
| #
cbf14186 |
|
22-Feb-2018 |
paulson <lp15@cam.ac.uk> |
type class linordered_nonzero_semiring has new axiom to guarantee characteristic 0
|
| #
c7cc1919 |
|
26-Nov-2017 |
wenzelm <none@none> |
more symbols;
|
| #
351cc2e6 |
|
17-Oct-2016 |
nipkow <none@none> |
setsum -> sum
|
| #
3a51760b |
|
19-Feb-2016 |
hoelzl <none@none> |
generalize more theorems to support enat and ennreal
--HG--
extra : rebase_source : 11176604a37483aa41462153f0aa289df506590d
|
| #
cef8f2ad |
|
10-Feb-2016 |
hoelzl <none@none> |
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.
--HG--
extra : rebase_source : 54bd3e5fcde04ef38241be91231c48d078b850f2
|
| #
995e8380 |
|
18-Feb-2016 |
hoelzl <none@none> |
remove lattice syntax from countable complete lattice
--HG--
extra : rebase_source : 32b8b96f528902b7294caefcc086deff59c968d9
|
| #
9242fadd |
|
11-Nov-2015 |
Andreas Lochbihler <none@none> |
add lemmas for extended nats and reals
|
| #
6c667f5f |
|
10-Oct-2015 |
wenzelm <none@none> |
prefer symbols;
|
| #
607ae3e3 |
|
09-Oct-2015 |
wenzelm <none@none> |
discontinued specific HTML syntax;
|
| #
85ed9565 |
|
01-Sep-2015 |
wenzelm <none@none> |
eliminated \<Colon>;
|
| #
94ea3a82 |
|
06-Jul-2015 |
wenzelm <none@none> |
tuned proofs;
|
| #
ab2206a7 |
|
03-Jul-2015 |
hoelzl <none@none> |
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
--HG--
extra : rebase_source : b8f67b531a15510b1f468145a6194cf68875d262
|
| #
a0af5cdd |
|
17-Jun-2015 |
wenzelm <none@none> |
isabelle update_cartouches;
|
| #
34035ccd |
|
04-Mar-2015 |
wenzelm <none@none> |
tuned signature -- prefer qualified names;
|
| #
dd06c109 |
|
09-Dec-2014 |
hoelzl <none@none> |
move topology on enat to Extended_Real, otherwise Jinja_Threads fails
--HG--
extra : rebase_source : cb6f2b3c00d194a2869610bb6a6b43dfa12cb3d5
extra : amend_source : 52d759bb82ad3475658070e4cfe7267e9ddcedc6
|
| #
9f8afd54 |
|
08-Dec-2014 |
hoelzl <none@none> |
instance bool and enat as topologies
|
| #
ff53cb2b |
|
13-Nov-2014 |
hoelzl <none@none> |
import general theorems from AFP/Markov_Models
|
| #
34a3534a |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header;
|
| #
cb40fd66 |
|
11-Sep-2014 |
blanchet <none@none> |
renamed 'rep_datatype' to 'old_rep_datatype' (HOL)
|
| #
38907e37 |
|
05-Jul-2014 |
haftmann <none@none> |
prefer ac_simps collections over separate name bindings for add and mult
|
| #
e46c07fd |
|
04-Jul-2014 |
haftmann <none@none> |
reduced name variants for assoc and commute on plus and mult
|
| #
4e59d26a |
|
28-Apr-2014 |
wenzelm <none@none> |
tuned;
|
| #
bcfbb56c |
|
12-Nov-2013 |
hoelzl <none@none> |
fix document generation for Extended_Nat
|
| #
ba10e8d5 |
|
12-Nov-2013 |
hoelzl <none@none> |
better support for enat and ereal conversions
|
| #
978fde4b |
|
12-Nov-2013 |
hoelzl <none@none> |
enat is countable
|
| #
1612e9ff |
|
25-Jul-2013 |
haftmann <none@none> |
factored syntactic type classes for bot and top (by Alessandro Coglio)
|
| #
0928b2db |
|
18-Apr-2013 |
wenzelm <none@none> |
simplifier uses proper Proof.context instead of historic type simpset;
|
| #
c38b4a86 |
|
06-Mar-2013 |
huffman <none@none> |
avoid using Arith_Data.dest_sum in extended-nat simprocs (it treats 'x - y' as 'x + - y', which is not valid for enat)
|
| #
e7aaf9d1 |
|
27-Feb-2013 |
wenzelm <none@none> |
simplified imports;
|
| #
2732ee62 |
|
31-Jan-2013 |
hoelzl <none@none> |
use order topology for extended reals
|
| #
d9333ba5 |
|
19-Oct-2012 |
webertj <none@none> |
Renamed {left,right}_distrib to distrib_{right,left}.
|
| #
c82bd4c5 |
|
12-Oct-2012 |
wenzelm <none@none> |
discontinued obsolete typedef (open) syntax;
|
| #
8bb6233a |
|
25-Mar-2012 |
huffman <none@none> |
merged fork with new numeral representation (see NEWS)
|
| #
efc317e6 |
|
20-Dec-2011 |
noschinl <none@none> |
add simp rules for enat and ereal
|
| #
1f882b8b |
|
07-Dec-2011 |
huffman <none@none> |
add cancellation simprocs for type enat
--HG--
extra : transplant_source : %D1%3F%0E%3C%BA%E4%88%D73%F1%A4%7C%3C3%F2%F4%C43%9E%0E
|
| #
054afeba |
|
16-Nov-2011 |
huffman <none@none> |
remove redundant simp rules plus_enat_0
|
| #
ad9e459c |
|
11-Sep-2011 |
nipkow <none@none> |
new fastforce replacing fastsimp - less confusing name
|
| #
841a5798 |
|
02-Aug-2011 |
huffman <none@none> |
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
|
| #
b671f9ef |
|
26-Jul-2011 |
hoelzl <none@none> |
enat is a complete_linorder instance
|
| #
b30e96e6 |
|
19-Jul-2011 |
hoelzl <none@none> |
rename Fin to enat
|
| #
aeae50c7 |
|
19-Jul-2011 |
hoelzl <none@none> |
add ereal to typeclass infinity
|
| #
075e0e17 |
|
19-Jul-2011 |
hoelzl <none@none> |
add nat => enat coercion
|
| #
18d52b47 |
|
19-Jul-2011 |
hoelzl <none@none> |
Introduce infinity type class
|
| #
d88e2f4a |
|
19-Jul-2011 |
hoelzl <none@none> |
rename Nat_Infinity (inat) to Extended_Nat (enat)
--HG--
rename : src/HOL/Library/Nat_Infinity.thy => src/HOL/Library/Extended_Nat.thy
|