| 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
|
| Tue, 12 Nov 2013 19:28:52 +0100 |
hoelzl |
stronger inc_induct and dec_induct
|
file |
diff |
annotate
|
| Tue, 05 Nov 2013 09:45:02 +0100 |
hoelzl |
move Lubs from HOL to HOL-Library (replaced by conditionally complete lattices)
|
file |
diff |
annotate
|
| Tue, 05 Nov 2013 09:44:58 +0100 |
hoelzl |
use bdd_above and bdd_below for conditionally complete lattices
|
file |
diff |
annotate
|
| Fri, 01 Nov 2013 18:51:14 +0100 |
haftmann |
more simplification rules on unary and binary minus
|
file |
diff |
annotate
|
| Tue, 24 Sep 2013 16:03:00 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Sat, 14 Sep 2013 22:30:10 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Sat, 14 Sep 2013 13:59:57 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Thu, 12 Sep 2013 18:09:17 -0700 |
huffman |
make 'linear' into a sublocale of 'bounded_linear';
|
file |
diff |
annotate
|
| Thu, 12 Sep 2013 09:39:02 -0700 |
huffman |
remove duplicate lemmas
|
file |
diff |
annotate
|
| Wed, 11 Sep 2013 00:00:59 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|