Thu, 14 Jun 2018 14:23:38 +0100 |
paulson |
reorganisation of Algebra: new material from Baillon and Vilhena, removal of duplicate names, elimination of "More_" theories
|
file |
diff |
annotate
|
Tue, 12 Jun 2018 16:08:57 +0100 |
paulson |
New material from Martin Baillon and Paulo EmÃlio de Vilhena
|
file |
diff |
annotate
|
Tue, 29 May 2018 14:05:59 +0200 |
nipkow |
canonical names
|
file |
diff |
annotate
|
Thu, 24 May 2018 14:42:47 +0200 |
nipkow |
reorganization, everything based on Tree2 now
|
file |
diff |
annotate
|
Sat, 12 May 2018 11:24:11 +0200 |
Andreas Lochbihler |
new tool Code_Lazy
|
file |
diff |
annotate
|
Wed, 09 May 2018 22:25:24 +0200 |
wenzelm |
less ambitious parallelism, notably for threads=2;
|
file |
diff |
annotate
|
Wed, 25 Apr 2018 13:29:21 +0000 |
haftmann |
proof of concept for residue rings over int using type numerals
|
file |
diff |
annotate
|
Tue, 24 Apr 2018 14:17:58 +0000 |
haftmann |
proper datatype for 8-bit characters
|
file |
diff |
annotate
|
Sun, 08 Apr 2018 11:05:52 +0200 |
nipkow |
more name tuning
|
file |
diff |
annotate
|
Wed, 21 Mar 2018 20:17:25 +0100 |
haftmann |
proof of concept for algebraically founded bit lists
|
file |
diff |
annotate
|
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
|