| 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
|