Fri, 04 Jan 2019 23:22:53 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
Wed, 31 Oct 2018 15:53:32 +0100 |
wenzelm |
clarified ML_Context.expression: it is a closed expression, not a let-declaration -- thus source positions are more accurate (amending d8849cfad60f, 162a4c2e97bc);
|
file |
diff |
annotate
|
Wed, 03 Oct 2018 10:42:00 +0100 |
paulson |
merged
|
file |
diff |
annotate
|
Mon, 24 Sep 2018 14:33:08 +0100 |
paulson |
cosmetic change to mvt
|
file |
diff |
annotate
|
Mon, 24 Sep 2018 14:30:09 +0200 |
nipkow |
Prefix form of infix with * on either side no longer needs special treatment
|
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
|
Mon, 16 Jul 2018 23:33:28 +0100 |
paulson |
de-applying and simplifying proofs
|
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
|
Tue, 10 Jul 2018 23:18:08 +0100 |
paulson |
de-applying, etc.
|
file |
diff |
annotate
|
Sat, 07 Jul 2018 15:07:37 +0100 |
paulson |
de-applying, etc.
|
file |
diff |
annotate
|
Thu, 28 Jun 2018 14:13:57 +0100 |
paulson |
Generalising and renaming some basic results
|
file |
diff |
annotate
|
Fri, 23 Feb 2018 14:56:32 +0000 |
Wenda Li |
merged
|
file |
diff |
annotate
|
Fri, 23 Feb 2018 13:27:19 +0000 |
Wenda Li |
Unified the order of zeros and poles; improved reasoning around non-essential singularites
|
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
|
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
|
Wed, 06 Dec 2017 20:43:09 +0100 |
wenzelm |
prefer control symbol antiquotations;
|
file |
diff |
annotate
|
Mon, 17 Oct 2016 17:33:07 +0200 |
nipkow |
setprod -> prod
|
file |
diff |
annotate
|
Mon, 17 Oct 2016 11:46:22 +0200 |
nipkow |
setsum -> sum
|
file |
diff |
annotate
|
Wed, 28 Sep 2016 17:01:01 +0100 |
paulson |
new material connected with HOL Light measure theory, plus more rationalisation
|
file |
diff |
annotate
|
Mon, 19 Sep 2016 20:06:21 +0200 |
fleury |
left_distrib ~> distrib_right, right_distrib ~> distrib_left
|
file |
diff |
annotate
|
Sun, 18 Sep 2016 20:33:48 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
Thu, 18 Aug 2016 18:11:45 +0200 |
hoelzl |
remove spurious find_theorems
|
file |
diff |
annotate
|
Wed, 17 Aug 2016 16:16:38 +0200 |
eberlm |
Tuned L'Hospital
|
file |
diff |
annotate
|
Wed, 10 Aug 2016 09:33:54 +0200 |
nipkow |
"split add" -> "split"
|
file |
diff |
annotate
|
Mon, 08 Aug 2016 14:13:14 +0200 |
hoelzl |
rename HOL-Multivariate_Analysis to HOL-Analysis.
|
file |
diff |
annotate
|
Thu, 28 Jul 2016 20:39:46 +0200 |
wenzelm |
misc tuning and modernization;
|
file |
diff |
annotate
|
Wed, 13 Jul 2016 17:14:17 +0100 |
paulson |
lots of new theorems about differentiable_on, retracts, ANRs, etc.
|
file |
diff |
annotate
|
Tue, 14 Jun 2016 13:14:11 +0200 |
eberlm |
Integration by substitution
|
file |
diff |
annotate
|
Thu, 09 Jun 2016 16:04:20 +0200 |
immler |
approximation, derivative, and continuity of floor and ceiling
|
file |
diff |
annotate
|
Fri, 27 May 2016 20:23:55 +0200 |
wenzelm |
tuned proofs, to allow unfold_abs_def;
|
file |
diff |
annotate
|
Fri, 13 May 2016 20:24:10 +0200 |
wenzelm |
eliminated use of empty "assms";
|
file |
diff |
annotate
|
Tue, 10 May 2016 15:48:37 +0200 |
immler |
some slight generalizations
|
file |
diff |
annotate
|
Mon, 25 Apr 2016 16:09:26 +0200 |
wenzelm |
eliminated old 'def';
|
file |
diff |
annotate
|
Wed, 24 Feb 2016 16:00:57 +0000 |
paulson |
Merge
|
file |
diff |
annotate
|
Wed, 24 Feb 2016 15:51:01 +0000 |
paulson |
Substantial new material for multivariate analysis. Also removal of some duplicates.
|
file |
diff |
annotate
|
Tue, 23 Feb 2016 16:25:08 +0100 |
nipkow |
more canonical names
|
file |
diff |
annotate
|
Wed, 30 Dec 2015 14:05:51 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
Wed, 30 Dec 2015 11:21:54 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
Wed, 09 Dec 2015 17:35:22 +0000 |
paulson |
sorted out eventually_mono
|
file |
diff |
annotate
|
Mon, 07 Dec 2015 10:38:04 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
Tue, 10 Nov 2015 14:18:41 +0000 |
paulson |
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
|
file |
diff |
annotate
|
Mon, 02 Nov 2015 16:17:09 +0100 |
eberlm |
Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
|
file |
diff |
annotate
|
Mon, 21 Sep 2015 19:52:13 +0100 |
paulson |
new lemmas and movement of lemmas into place
|
file |
diff |
annotate
|
Sat, 18 Jul 2015 22:58:50 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
Tue, 05 May 2015 18:45:10 +0200 |
immler |
moved basic lemmas about has_vector_derivative
|
file |
diff |
annotate
|
Tue, 31 Mar 2015 21:54:32 +0200 |
haftmann |
given up separate type classes demanding `inverse 0 = 0`
|
file |
diff |
annotate
|
Tue, 31 Mar 2015 15:00:03 +0100 |
paulson |
New material and binomial fix
|
file |
diff |
annotate
|
Fri, 06 Mar 2015 12:48:03 +0000 |
paulson |
A few new lemmas and a bit of tidying up
|
file |
diff |
annotate
|
Sun, 02 Nov 2014 18:21:45 +0100 |
wenzelm |
modernized header uniformly as section;
|
file |
diff |
annotate
|
Mon, 20 Oct 2014 18:33:14 +0200 |
hoelzl |
add tendsto_const and tendsto_ident_at as simp and intro rules
|
file |
diff |
annotate
|
Sat, 16 Aug 2014 14:42:35 +0200 |
wenzelm |
updated to named_theorems;
|
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
|
Sat, 28 Jun 2014 09:16:42 +0200 |
haftmann |
fact consolidation
|
file |
diff |
annotate
|
Fri, 11 Apr 2014 22:53:33 +0200 |
nipkow |
made divide_pos_pos a simp rule
|
file |
diff |
annotate
|
Wed, 09 Apr 2014 09:37:48 +0200 |
hoelzl |
field_simps: better support for negation and division, and power
|
file |
diff |
annotate
|