| #
711c1878 |
|
30-Oct-2017 |
haftmann <none@none> |
tuned some proofs and added some lemmas
--HG--
extra : rebase_source : ad93f195ceb7a124396a911453e61f00f52999be
|
| #
1d1ca5f1 |
|
08-Oct-2017 |
haftmann <none@none> |
avoid name clashes on interpretation of abstract locales
--HG--
extra : rebase_source : f524b077cafad9e920061f751ff3126d7a903434
|
| #
351cc2e6 |
|
17-Oct-2016 |
nipkow <none@none> |
setsum -> sum
|
| #
9a8c3fb3 |
|
19-Sep-2016 |
fleury <Mathias.Fleury@mpi-inf.mpg.de> |
left_distrib ~> distrib_right, right_distrib ~> distrib_left
|
| #
3dba35c1 |
|
27-May-2016 |
wenzelm <none@none> |
tuned proofs, to allow unfold_abs_def;
|
| #
e3b38c13 |
|
17-Feb-2016 |
haftmann <none@none> |
dropped various legacy fact bindings
|
| #
4b76bc27 |
|
01-Dec-2015 |
paulson <lp15@cam.ac.uk> |
Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
|
| #
53483153 |
|
16-Nov-2015 |
paulson <lp15@cam.ac.uk> |
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
|
| #
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.
|
| #
3f106d8a |
|
10-Nov-2015 |
paulson <lp15@cam.ac.uk> |
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
|
| #
1901affb |
|
18-Jul-2015 |
wenzelm <none@none> |
isabelle update_cartouches;
|
| #
73115e7b |
|
01-May-2015 |
nipkow <none@none> |
simplified statement and proof
|
| #
587e133b |
|
28-Apr-2015 |
paulson <lp15@cam.ac.uk> |
New material about complex transcendental functions (especially Ln, Arg) and polynomials
|
| #
17332b93 |
|
16-Mar-2015 |
wenzelm <none@none> |
proper headers;
|
| #
57ed09d5 |
|
16-Mar-2015 |
hoelzl <none@none> |
add inequalities (move from AFP/Amortized_Complexity)
|