| Wed, 14 Feb 2018 16:32:09 +0100 |
nipkow |
New theory ex/Radix_Sort.thy
|
file |
diff |
annotate
|
| Wed, 14 Feb 2018 11:51:03 +0100 |
Lars Hupel |
records based on datatypes/BNF infrastructure
|
file |
diff |
annotate
|
| Tue, 02 Jan 2018 16:17:13 +0100 |
blanchet |
moved 'realizers' into their own theory, now that they are decupled from the old datatype construction
|
file |
diff |
annotate
|
| Sun, 24 Dec 2017 14:28:10 +0100 |
eberlm |
Removed Analysis/ex/Circle_Area; replaced by more general Analysis/Ball_Volume
|
file |
diff |
annotate
|
| Mon, 18 Dec 2017 16:58:13 +0100 |
traytel |
a conditional paramitrecity prover
|
file |
diff |
annotate
|
| Sat, 16 Dec 2017 16:46:01 +0100 |
wenzelm |
PIDE markup for session ROOT files;
|
file |
diff |
annotate
|
| Thu, 07 Dec 2017 20:55:03 +0100 |
wenzelm |
more robust;
|
file |
diff |
annotate
|
| 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
|
| Wed, 07 Jun 2017 20:18:23 +0200 |
wenzelm |
clarified imports;
|
file |
diff |
annotate
|
| Mon, 05 Jun 2017 15:59:45 +0200 |
haftmann |
specific output setup is not supposed to intrude regular import theory
|
file |
diff |
annotate
|
| Mon, 29 May 2017 09:14:15 +0200 |
eberlm |
reorganised material on sublists
|
file |
diff |
annotate
|
| Tue, 02 May 2017 10:47:39 +0200 |
wenzelm |
more timing;
|
file |
diff |
annotate
|
| Mon, 24 Apr 2017 23:10:01 +0200 |
wenzelm |
recovered document from 0f3fdf689bf9;
|
file |
diff |
annotate
|
| Mon, 24 Apr 2017 13:58:38 +0200 |
wenzelm |
clarified parent session images, to avoid duplicate loading of theories;
|
file |
diff |
annotate
|
| Mon, 24 Apr 2017 11:52:51 +0200 |
wenzelm |
clarified parent session images, to avoid duplicate loading of theories;
|
file |
diff |
annotate
|
| Sun, 23 Apr 2017 23:54:06 +0200 |
wenzelm |
actually use theory;
|
file |
diff |
annotate
|
| Sun, 23 Apr 2017 23:49:14 +0200 |
wenzelm |
clarified parent session images, to avoid duplicate loading of theories;
|
file |
diff |
annotate
|
| Sun, 23 Apr 2017 19:06:53 +0200 |
wenzelm |
actually use theory;
|
file |
diff |
annotate
|
| Sun, 23 Apr 2017 18:54:18 +0200 |
wenzelm |
renamed theory to avoid conflict with loaded theory "Tree" from HOL-Library;
|
file |
diff |
annotate
|
| Sat, 22 Apr 2017 22:01:35 +0200 |
wenzelm |
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
|
file |
diff |
annotate
|
| Sat, 22 Apr 2017 12:52:16 +0200 |
wenzelm |
clarified parent session images, to avoid duplicate loading of theories;
|
file |
diff |
annotate
|
| Fri, 21 Apr 2017 21:41:32 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 21 Apr 2017 21:36:49 +0200 |
wenzelm |
removed pointless document;
|
file |
diff |
annotate
|
| Fri, 21 Apr 2017 20:36:20 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Fri, 21 Apr 2017 20:07:51 +0200 |
wenzelm |
clarified session imports;
|
file |
diff |
annotate
|
| Fri, 21 Apr 2017 16:48:58 +0200 |
wenzelm |
tuned imports;
|
file |
diff |
annotate
|
| Fri, 21 Apr 2017 16:12:11 +0200 |
wenzelm |
clarified imports;
|
file |
diff |
annotate
|
| Fri, 21 Apr 2017 11:38:45 +0200 |
wenzelm |
include imports that morally belong to Main and are used in HOL-Proofs applications;
|
file |
diff |
annotate
|
| Thu, 20 Apr 2017 16:21:28 +0200 |
blanchet |
removed Old_SMT legacy module
|
file |
diff |
annotate
|
| Wed, 19 Apr 2017 15:53:58 +0200 |
wenzelm |
clarified session structure: avoid ambiguity of file ~~/src/HOL/Library/Old_Datatype.thy;
|
file |
diff |
annotate
|
| Mon, 17 Apr 2017 07:44:21 +0200 |
haftmann |
consistent session name
|
file |
diff |
annotate
|