| Wed, 06 Dec 2017 21:43:20 +0100 |
wenzelm |
just one session for bulky HOL-Analysis documents;
|
file |
diff |
annotate
|
| Sun, 03 Dec 2017 19:09:42 +0100 |
wenzelm |
simplified session (again, see 39e29972cb96): WordExamples requires < 1s;
|
file |
diff |
annotate
|
| Mon, 27 Nov 2017 16:18:29 +0100 |
wenzelm |
clarified main sessions;
|
file |
diff |
annotate
|
| Tue, 07 Nov 2017 14:52:27 +0100 |
nipkow |
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
|
file |
diff |
annotate
|
| Fri, 03 Nov 2017 13:43:31 +0100 |
wenzelm |
less global theories -- avoid confusion about special cases;
|
file |
diff |
annotate
|
| Wed, 01 Nov 2017 22:13:38 +0100 |
wenzelm |
more timing;
|
file |
diff |
annotate
|
| Wed, 01 Nov 2017 18:37:49 +0100 |
wenzelm |
build faster without heap images for minor imports;
|
file |
diff |
annotate
|
| Tue, 31 Oct 2017 15:13:08 +0100 |
wenzelm |
no censorship (in contrast to 2c828c830ad7);
|
file |
diff |
annotate
|
| Tue, 31 Oct 2017 07:11:03 +0000 |
haftmann |
removed ancient nat-int transfer
|
file |
diff |
annotate
|
| Mon, 30 Oct 2017 20:26:19 +0100 |
wenzelm |
recovered document from 9bfb6978eb80;
|
file |
diff |
annotate
|
| Mon, 30 Oct 2017 20:04:10 +0100 |
wenzelm |
ROOT cleanup: empty 'document_files' means there is no document;
|
file |
diff |
annotate
|
| Sat, 28 Oct 2017 21:26:51 +0200 |
wenzelm |
reduced heap hierarchy, for potentially improved performance;
|
file |
diff |
annotate
|
| Wed, 11 Oct 2017 20:46:38 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 08 Oct 2017 22:28:21 +0200 |
haftmann |
Polynomial_Factorial does not depend on Field_as_Ring as such
|
file |
diff |
annotate
|
| Sun, 08 Oct 2017 22:28:19 +0200 |
haftmann |
removed mere toy example from library
|
file |
diff |
annotate
|
| Sat, 07 Oct 2017 20:20:03 +0200 |
wenzelm |
clarified session structure;
|
file |
diff |
annotate
|
| Mon, 02 Oct 2017 19:38:39 +0200 |
wenzelm |
prefer file dependencies wrt. specific theories;
|
file |
diff |
annotate
|
| Mon, 02 Oct 2017 18:35:51 +0200 |
wenzelm |
proper document (cf. 9f5bfef8bd82);
|
file |
diff |
annotate
|
| Mon, 02 Oct 2017 18:11:28 +0200 |
wenzelm |
removed pointless dependencies: done by 'spark_open';
|
file |
diff |
annotate
|
| Mon, 02 Oct 2017 16:41:59 +0200 |
wenzelm |
clarified imports: prefer parent session images;
|
file |
diff |
annotate
|
| Mon, 02 Oct 2017 16:08:43 +0200 |
wenzelm |
eliminated old-style no-document imports;
|
file |
diff |
annotate
|
| Fri, 08 Sep 2017 02:22:58 +0200 |
blanchet |
removed obsolete session
|
file |
diff |
annotate
|
| Thu, 31 Aug 2017 14:32:23 +0200 |
nipkow |
Moved material into AFP/Splay_Tree
|
file |
diff |
annotate
|
| Tue, 29 Aug 2017 12:05:00 +0200 |
nipkow |
new file
|
file |
diff |
annotate
|
| Fri, 18 Aug 2017 20:47:47 +0200 |
wenzelm |
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
|
file |
diff |
annotate
|
| Thu, 17 Aug 2017 14:40:42 +0200 |
wenzelm |
more complete session (amending e77ea0ea7f2c);
|
file |
diff |
annotate
|
| Thu, 17 Aug 2017 14:28:01 +0200 |
wenzelm |
clarified imports;
|
file |
diff |
annotate
|
| Thu, 17 Aug 2017 14:13:34 +0200 |
wenzelm |
more complete session (amending 783861a66a60);
|
file |
diff |
annotate
|
| Tue, 15 Aug 2017 19:47:08 +0200 |
nipkow |
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
|
file |
diff |
annotate
|
| Tue, 11 Jul 2017 17:22:33 +0200 |
Lars Hupel |
State_Monad ~> Open_State_Syntax
|
file |
diff |
annotate
|