| Thu, 08 Nov 2018 22:29:09 +0100 |
wenzelm |
isabelle update_cartouches -t;
|
file |
diff |
annotate
|
| Sun, 21 Oct 2018 09:39:09 +0200 |
nipkow |
uniform naming of strong congruence rules
|
file |
diff |
annotate
|
| Thu, 20 Sep 2018 18:20:02 +0100 |
paulson |
removal of more redundancies, and fixes
|
file |
diff |
annotate
|
| Thu, 20 Sep 2018 14:17:58 +0100 |
paulson |
elimination of near duplication involving Rolle's theorem and the MVT
|
file |
diff |
annotate
|
| Fri, 17 Aug 2018 11:26:35 +0000 |
haftmann |
proper code abbreviation for power on real
|
file |
diff |
annotate
|
| Mon, 16 Jul 2018 15:24:06 +0200 |
Manuel Eberl |
Made simproc for sqrt/root of numeral more robust
|
file |
diff |
annotate
|
| Sun, 15 Jul 2018 21:58:50 +0100 |
paulson |
de-applying and meta-quantifying
|
file |
diff |
annotate
|
| Sun, 15 Jul 2018 16:05:38 +0100 |
paulson |
fixes and more de-applying
|
file |
diff |
annotate
|
| Sun, 15 Jul 2018 13:15:31 +0100 |
paulson |
more de-applying and a fix
|
file |
diff |
annotate
|
| Wed, 11 Jul 2018 15:36:12 +0100 |
paulson |
more de-applying
|
file |
diff |
annotate
|
| Tue, 10 Jul 2018 23:18:08 +0100 |
paulson |
de-applying, etc.
|
file |
diff |
annotate
|
| Sun, 08 Jul 2018 11:00:20 +0100 |
paulson |
De-applying
|
file |
diff |
annotate
|
| Sat, 07 Jul 2018 15:07:37 +0100 |
paulson |
de-applying, etc.
|
file |
diff |
annotate
|
| Thu, 05 Jul 2018 23:37:00 +0100 |
paulson |
de-applying
|
file |
diff |
annotate
|
| Thu, 28 Jun 2018 14:13:57 +0100 |
paulson |
Generalising and renaming some basic results
|
file |
diff |
annotate
|
| Tue, 26 Jun 2018 14:51:18 +0100 |
paulson |
Rationalisation of complex transcendentals, esp the Arg function
|
file |
diff |
annotate
|
| Sun, 06 May 2018 18:20:25 +0000 |
haftmann |
removed some lemma duplicates
|
file |
diff |
annotate
|
| Thu, 03 May 2018 22:34:49 +0100 |
paulson |
Some tidying up (mostly regarding summations from 0)
|
file |
diff |
annotate
|
| Mon, 26 Feb 2018 07:34:05 +0100 |
immler |
moved Lipschitz continuity from AFP/Ordinary_Differential_Equations and AFP/Gromov_Hyperbolicity; moved lemmas from AFP/Gromov_Hyperbolicity/Library_Complements
|
file |
diff |
annotate
|
| Thu, 22 Feb 2018 15:17:25 +0100 |
immler |
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
|
file |
diff |
annotate
|
| Wed, 07 Feb 2018 18:08:12 +0100 |
eberlm |
Added hyperbolic functions
|
file |
diff |
annotate
|
| Mon, 05 Feb 2018 08:30:19 +0100 |
immler |
added lemmas, avoid 'float_of 0'
|
file |
diff |
annotate
|
| Tue, 16 Jan 2018 09:30:00 +0100 |
wenzelm |
standardized towards new-style formal comments: isabelle update_comments;
|
file |
diff |
annotate
|
| Wed, 10 Jan 2018 15:25:09 +0100 |
nipkow |
ran isabelle update_op on all sources
|
file |
diff |
annotate
|
| Fri, 22 Dec 2017 21:00:07 +0000 |
paulson |
new/improved theories involving convergence; better pretty-printing for bounded quantifiers and sum/product
|
file |
diff |
annotate
|
| Sun, 26 Nov 2017 21:08:32 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Tue, 10 Oct 2017 17:15:37 +0100 |
paulson |
Divided Topology_Euclidean_Space in two, creating new theory Connected. Also deleted some duplicate / variant theorems
|
file |
diff |
annotate
|
| Sun, 27 Aug 2017 13:02:13 +0200 |
nipkow |
tuned
|
file |
diff |
annotate
|
| Sat, 26 Aug 2017 16:47:25 +0200 |
nipkow |
reorganized and added log-related lemmas
|
file |
diff |
annotate
|
| Sat, 26 Aug 2017 09:10:42 +0200 |
nipkow |
tuned proofs
|
file |
diff |
annotate
|