| Mon, 21 Jan 2019 14:44:23 +0000 |
paulson |
new material about summations and powers, along with some tweaks
|
file |
diff |
annotate
|
| Mon, 14 Jan 2019 18:35:03 +0000 |
haftmann |
tuned proofs
|
file |
diff |
annotate
|
| Sun, 06 Jan 2019 15:04:34 +0100 |
wenzelm |
isabelle update -u path_cartouches;
|
file |
diff |
annotate
|
| Fri, 04 Jan 2019 23:22:53 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Thu, 12 Jul 2018 17:22:39 +0100 |
paulson |
de-applying (mostly Set_Interval)
|
file |
diff |
annotate
|
| Wed, 11 Jul 2018 01:04:23 +0200 |
nipkow |
moved lemmas
|
file |
diff |
annotate
|
| Fri, 23 Feb 2018 09:28:14 +0000 |
paulson |
fixing ennreal using add_mono1; shifting results from linordered_semidom to linordered_nonzero_semiring
|
file |
diff |
annotate
|
| Mon, 19 Feb 2018 16:44:45 +0000 |
paulson |
lots of new material, ultimately related to measure theory
|
file |
diff |
annotate
|
| Wed, 10 Jan 2018 15:25:09 +0100 |
nipkow |
ran isabelle update_op on all sources
|
file |
diff |
annotate
|
| Wed, 03 Jan 2018 11:06:13 +0100 |
blanchet |
kill old size infrastructure
|
file |
diff |
annotate
|
| Sun, 26 Nov 2017 21:08:32 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Sat, 11 Nov 2017 18:33:35 +0000 |
haftmann |
more induct rules on nat
|
file |
diff |
annotate
|
| Mon, 30 Oct 2017 19:29:06 +0000 |
haftmann |
added lemma
|
file |
diff |
annotate
|
| Mon, 30 Oct 2017 13:18:41 +0000 |
haftmann |
tuned some proofs and added some lemmas
|
file |
diff |
annotate
|
| Sun, 08 Oct 2017 22:28:22 +0200 |
haftmann |
more fundamental definition of div and mod on int
|
file |
diff |
annotate
|
| Sun, 08 Oct 2017 22:28:21 +0200 |
haftmann |
generalized simproc
|
file |
diff |
annotate
|
| Wed, 09 Aug 2017 12:01:16 +0200 |
nipkow |
added lemmas
|
file |
diff |
annotate
|
| Wed, 26 Jul 2017 13:36:36 +0100 |
paulson |
moved transitive_stepwise_le into Nat, where it belongs
|
file |
diff |
annotate
|
| Thu, 20 Jul 2017 16:28:43 +0100 |
blanchet |
strengthened tactic
|
file |
diff |
annotate
|
| Tue, 30 May 2017 14:04:48 +0200 |
nipkow |
tuned names
|
file |
diff |
annotate
|
| Tue, 30 May 2017 10:03:35 +0200 |
nipkow |
redefined Greatest
|
file |
diff |
annotate
|
| Wed, 26 Apr 2017 15:53:35 +0100 |
paulson |
Further new material. The simprule status of some exp and ln identities was reverted.
|
file |
diff |
annotate
|
| Wed, 11 Jan 2017 16:43:31 +0100 |
blanchet |
generalized types in lemmas
|
file |
diff |
annotate
|
| Mon, 09 Jan 2017 18:53:20 +0100 |
haftmann |
moved some lemmas to appropriate places
|
file |
diff |
annotate
|
| Fri, 30 Dec 2016 18:02:27 +0100 |
haftmann |
dropped slightly outdated comment
|
file |
diff |
annotate
|
| Tue, 22 Nov 2016 18:36:59 +0100 |
nipkow |
added lemma
|
file |
diff |
annotate
|
| Sat, 01 Oct 2016 17:16:35 +0200 |
wenzelm |
clarified lfp/gfp statements and proofs;
|
file |
diff |
annotate
|
| Wed, 10 Aug 2016 09:33:54 +0200 |
nipkow |
"split add" -> "split"
|
file |
diff |
annotate
|
| Tue, 02 Aug 2016 21:05:34 +0200 |
wenzelm |
misc tuning and modernization;
|
file |
diff |
annotate
|
| Fri, 29 Jul 2016 09:49:23 +0200 |
Andreas Lochbihler |
add lemmas contributed by Peter Gammie
|
file |
diff |
annotate
|