Mon, 21 Sep 2015 19:52:13 +0100 |
paulson |
new lemmas and movement of lemmas into place
|
file |
diff |
annotate
|
Sun, 13 Sep 2015 21:06:58 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
Sun, 13 Sep 2015 20:20:16 +0200 |
wenzelm |
renamed method "goals" to "goal_cases" to emphasize its meaning;
|
file |
diff |
annotate
|
Sun, 13 Sep 2015 16:50:12 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
Tue, 01 Sep 2015 22:32:58 +0200 |
wenzelm |
eliminated \<Colon>;
|
file |
diff |
annotate
|
Thu, 06 Aug 2015 23:56:48 +0200 |
haftmann |
slight cleanup of lemmas
|
file |
diff |
annotate
|
Tue, 28 Jul 2015 17:15:01 +0100 |
paulson |
tweaks. Got rid of a really slow step
|
file |
diff |
annotate
|
Mon, 27 Jul 2015 16:52:57 +0100 |
paulson |
New material for Cauchy's integral theorem
|
file |
diff |
annotate
|
Mon, 20 Jul 2015 23:12:50 +0100 |
paulson |
new material for multivariate analysis, etc.
|
file |
diff |
annotate
|
Wed, 01 Jul 2015 13:09:56 +0200 |
immler |
taylor series with has_integral and integrable_on
|
file |
diff |
annotate
|
Tue, 30 Jun 2015 13:56:16 +0100 |
paulson |
Useful lemmas. The theorem concerning swapping the variables in a double integral.
|
file |
diff |
annotate
|
Fri, 26 Jun 2015 10:20:33 +0200 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
Tue, 16 Jun 2015 20:50:00 +0100 |
paulson |
another messy proof fixed
|
file |
diff |
annotate
|
Mon, 15 Jun 2015 21:33:26 +0100 |
paulson |
inverted another messy proof
|
file |
diff |
annotate
|
Sun, 14 Jun 2015 18:51:34 +0100 |
paulson |
another tangled proof
|
file |
diff |
annotate
|
Sun, 14 Jun 2015 17:05:27 +0100 |
paulson |
Tidied up more proofs
|
file |
diff |
annotate
|
Sun, 14 Jun 2015 14:25:01 +0100 |
paulson |
another proof
|
file |
diff |
annotate
|
Sun, 14 Jun 2015 12:48:32 +0100 |
paulson |
fixing more proofs
|
file |
diff |
annotate
|
Sat, 13 Jun 2015 22:48:47 +0100 |
paulson |
fixed another horrible proof
|
file |
diff |
annotate
|
Sat, 13 Jun 2015 19:23:41 +0100 |
paulson |
streamlined many more proofs
|
file |
diff |
annotate
|
Sat, 13 Jun 2015 12:30:12 +0100 |
paulson |
tidied more proofs
|
file |
diff |
annotate
|
Sat, 13 Jun 2015 00:33:14 +0100 |
paulson |
proof tidying
|
file |
diff |
annotate
|
Thu, 11 Jun 2015 21:41:55 +0100 |
paulson |
fixed several "inside-out" proofs
|
file |
diff |
annotate
|
Thu, 11 Jun 2015 00:12:27 +0100 |
paulson |
tidied more proofs
|
file |
diff |
annotate
|
Wed, 10 Jun 2015 19:10:20 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
Tue, 09 Jun 2015 22:48:11 +0100 |
paulson |
more tidying up of proofs
|
file |
diff |
annotate
|
Mon, 08 Jun 2015 23:51:08 +0100 |
paulson |
tidying messy proofs
|
file |
diff |
annotate
|
Mon, 08 Jun 2015 00:25:10 +0100 |
paulson |
Tidied lots of messy proofs
|
file |
diff |
annotate
|
Tue, 05 May 2015 18:45:10 +0200 |
immler |
general Taylor series expansion with integral remainder
|
file |
diff |
annotate
|
Fri, 20 Mar 2015 16:11:28 +0000 |
paulson |
tweaked a few slow or very ugly proofs
|
file |
diff |
annotate
|
Sat, 07 Mar 2015 21:32:31 +0100 |
wenzelm |
clarified Drule.gen_all: observe context more carefully;
|
file |
diff |
annotate
|
Thu, 22 Jan 2015 14:51:08 +0100 |
hoelzl |
import general thms from Density_Compiler
|
file |
diff |
annotate
|
Sun, 02 Nov 2014 17:09:04 +0100 |
wenzelm |
modernized header;
|
file |
diff |
annotate
|
Sun, 21 Sep 2014 16:56:11 +0200 |
haftmann |
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
|
file |
diff |
annotate
|
Tue, 05 Aug 2014 16:58:19 +0200 |
wenzelm |
tuned proofs -- fewer warnings;
|
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
|
Mon, 30 Jun 2014 15:45:21 +0200 |
hoelzl |
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
|
file |
diff |
annotate
|
Sat, 28 Jun 2014 09:16:42 +0200 |
haftmann |
fact consolidation
|
file |
diff |
annotate
|
Fri, 30 May 2014 14:55:10 +0200 |
hoelzl |
introduce more powerful reindexing rules for big operators
|
file |
diff |
annotate
|
Sat, 12 Apr 2014 17:26:27 +0200 |
nipkow |
made mult_pos_pos a simp rule
|
file |
diff |
annotate
|
Fri, 11 Apr 2014 22:53:33 +0200 |
nipkow |
made divide_pos_pos a simp rule
|
file |
diff |
annotate
|
Fri, 11 Apr 2014 13:36:57 +0200 |
nipkow |
made mult_nonneg_nonneg a simp rule
|
file |
diff |
annotate
|
Thu, 03 Apr 2014 17:56:08 +0200 |
hoelzl |
merged DERIV_intros, has_derivative_intros into derivative_intros
|
file |
diff |
annotate
|
Wed, 02 Apr 2014 18:35:07 +0200 |
hoelzl |
extend continuous_intros; remove continuous_on_intros and isCont_intros
|
file |
diff |
annotate
|
Mon, 31 Mar 2014 17:17:37 +0200 |
hoelzl |
tuned proofs
|
file |
diff |
annotate
|
Wed, 19 Mar 2014 18:47:22 +0100 |
haftmann |
elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
|
file |
diff |
annotate
|
Tue, 18 Mar 2014 15:53:48 +0100 |
hoelzl |
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
|
file |
diff |
annotate
|
Tue, 18 Mar 2014 10:12:58 +0100 |
immler |
additional lemmas
|
file |
diff |
annotate
|
Tue, 18 Mar 2014 10:12:58 +0100 |
immler |
removed dependencies on theory Ordered_Euclidean_Space
|
file |
diff |
annotate
|
Tue, 18 Mar 2014 10:12:57 +0100 |
immler |
use cbox to relax class constraints
|
file |
diff |
annotate
|
Mon, 17 Mar 2014 19:12:52 +0100 |
hoelzl |
unify syntax for has_derivative and differentiable
|
file |
diff |
annotate
|
Mon, 17 Mar 2014 18:06:59 +0100 |
haftmann |
tuned proofs
|
file |
diff |
annotate
|
Sun, 16 Mar 2014 18:09:04 +0100 |
haftmann |
normalising simp rules for compound operators
|
file |
diff |
annotate
|
Tue, 25 Feb 2014 21:58:46 +0100 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
Wed, 12 Feb 2014 08:37:06 +0100 |
blanchet |
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
|
file |
diff |
annotate
|
Wed, 25 Dec 2013 17:39:06 +0100 |
haftmann |
prefer more canonical names for lemmas on min/max
|
file |
diff |
annotate
|
Mon, 16 Dec 2013 17:08:22 +0100 |
immler |
additional lemmas
|
file |
diff |
annotate
|
Mon, 16 Dec 2013 17:08:22 +0100 |
immler |
remove redundant constants
|
file |
diff |
annotate
|
Mon, 16 Dec 2013 17:08:22 +0100 |
immler |
ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
|
file |
diff |
annotate
|
Mon, 16 Dec 2013 17:08:22 +0100 |
immler |
prefer box over greaterThanLessThan on euclidean_space
|
file |
diff |
annotate
|