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