| #
102fb118 |
|
26-Jun-2018 |
paulson <lp15@cam.ac.uk> |
Rationalisation of complex transcendentals, esp the Arg function
|
| #
5c09067f |
|
09-Oct-2017 |
paulson <lp15@cam.ac.uk> |
new material about connectedness, etc.
|
| #
5ba2adde |
|
26-Aug-2017 |
nipkow <none@none> |
reorganized and added log-related lemmas
|
| #
4e103b68 |
|
21-Jun-2017 |
paulson <lp15@cam.ac.uk> |
Tidying up integration theory and some new theorems
|
| #
908a5437 |
|
20-Oct-2016 |
eberlm <eberlm@in.tum.de> |
More on Fibonacci numbers
--HG--
extra : amend_source : 20377014e72d63c52d11330a6ce94cab4990294e
|
| #
db6d6915 |
|
27-Sep-2016 |
paulson <lp15@cam.ac.uk> |
a few new theorems and a renaming
|
| #
1e83a38a |
|
15-Sep-2016 |
paulson <lp15@cam.ac.uk> |
simple new lemmas, mostly about sets
|
| #
78916208 |
|
06-Aug-2016 |
nipkow <none@none> |
tuned
|
| #
39d2c0cc |
|
04-Aug-2016 |
nipkow <none@none> |
fixed floor proofs
|
| #
64974886 |
|
05-Aug-2016 |
nipkow <none@none> |
tuned floor lemmas
|
| #
14001a0d |
|
22-Jul-2016 |
wenzelm <none@none> |
tuned proofs -- avoid unstructured calculation;
|
| #
7655367b |
|
14-Jul-2016 |
wenzelm <none@none> |
misc tuning and modernization;
|
| #
13683eca |
|
17-Jun-2016 |
hoelzl <none@none> |
move Conditional_Complete_Lattices to Main
--HG--
extra : rebase_source : 2cd0f07680d0081b5d3769e8a4ad49983a312a99
|
| #
db1c38d3 |
|
15-Mar-2016 |
paulson <lp15@cam.ac.uk> |
rationalisation of theorem names esp about "real Archimedian" etc.
|
| #
e3b38c13 |
|
17-Feb-2016 |
haftmann <none@none> |
dropped various legacy fact bindings
|
| #
08cabf03 |
|
27-Dec-2015 |
wenzelm <none@none> |
prefer symbols for "abs";
|
| #
ecc07c37 |
|
27-Dec-2015 |
wenzelm <none@none> |
prefer symbols for "floor", "ceiling";
|
| #
3dc932ef |
|
23-Nov-2015 |
paulson <lp15@cam.ac.uk> |
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
|
| #
420aaf4c |
|
12-Nov-2015 |
paulson <lp15@cam.ac.uk> |
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
|
| #
dd88f1ec |
|
02-Nov-2015 |
eberlm <none@none> |
Rounding function, uniform limits, cotangent, binomial identities
|
| #
607ae3e3 |
|
09-Oct-2015 |
wenzelm <none@none> |
discontinued specific HTML syntax;
|
| #
78ffd573 |
|
31-Aug-2015 |
wenzelm <none@none> |
prefer symbols;
|
| #
1901affb |
|
18-Jul-2015 |
wenzelm <none@none> |
isabelle update_cartouches;
|
| #
3ee23ab1 |
|
17-Apr-2015 |
haftmann <none@none> |
compactified proposition
--HG--
extra : rebase_source : 50aa98e81c3a3e33838415042a87653811186df8
|
| #
9fdf6e80 |
|
09-Apr-2015 |
haftmann <none@none> |
conversion between division on nat/int and division in archmedean fields
|
| #
b5ab68e6 |
|
05-Mar-2015 |
paulson <lp15@cam.ac.uk> |
The function frac. Various lemmas about limits, series, the exp function, etc.
|
| #
794edf80 |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header uniformly as section;
|
| #
53400fc4 |
|
29-Aug-2014 |
hoelzl <none@none> |
add simp rules for divisions of numerals in floor and ceiling.
--HG--
extra : rebase_source : ea537029d27222136caea445ff8f1f5f6c3ff58c
|
| #
d285560c |
|
19-Aug-2014 |
hoelzl <none@none> |
better linarith support for floor, ceiling, natfloor, and natceiling
--HG--
extra : rebase_source : fac55dc42162d71e9d329d10d498c370b963de40
|
| #
138816de |
|
19-Nov-2013 |
haftmann <none@none> |
eliminiated neg_numeral in favour of - (numeral _)
|
| #
dddd44d5 |
|
05-Nov-2013 |
hoelzl <none@none> |
int and nat are conditionally_complete_lattices
--HG--
extra : rebase_source : 4295ba08a6a68dc20cc2a24971781ce06b986aac
|
| #
2d119c4c |
|
18-Apr-2012 |
hoelzl <none@none> |
add ceiling_diff_floor_le_1
--HG--
extra : rebase_source : c77d1e680dea5466f4d9ef77a63bf31db99d12f9
|
| #
50ddce1f |
|
03-Apr-2012 |
huffman <none@none> |
add floor/ceiling lemmas suggested by René Thiemann
|
| #
8bb6233a |
|
25-Mar-2012 |
huffman <none@none> |
merged fork with new numeral representation (see NEWS)
|
| #
29f8fb3e |
|
09-Jul-2011 |
bulwahn <none@none> |
adding code equations to execute floor and ceiling on rational and real numbers
|
| #
4f5acb61 |
|
09-Jul-2011 |
bulwahn <none@none> |
adding a floor_ceiling type class for different instantiations of floor (changeset from Brian Huffman)
|
| #
df034c97 |
|
07-Jul-2011 |
bulwahn <none@none> |
floor and ceiling definitions are not code equations -- this enables trivial evaluation of floor and ceiling
|
| #
6b0b29ec |
|
13-Mar-2011 |
wenzelm <none@none> |
tuned headers;
|
| #
55a5de32 |
|
12-Jul-2010 |
haftmann <none@none> |
dropped superfluous [code del]s
|
| #
5d17693c |
|
05-Feb-2010 |
haftmann <none@none> |
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
|
| #
3f2dddb8 |
|
26-Feb-2009 |
huffman <none@none> |
disable floor_minus and ceiling_minus [simp]
|
| #
4e32394e |
|
25-Feb-2009 |
huffman <none@none> |
new theory of Archimedean fields
|