| Sun, 13 Oct 2019 16:26:31 +0200 |
wenzelm |
clarified sessions/directories;
|
file |
diff |
annotate
|
| Mon, 07 Oct 2019 11:35:43 +0200 |
wenzelm |
discontinued pointless dump_checkpoint and share_common_data -- superseded by base logic image in Isabelle/MMT;
|
file |
diff |
annotate
|
| Wed, 02 Oct 2019 20:58:09 +0200 |
wenzelm |
just one dump_checkpoint Main -- potentially more robust;
|
file |
diff |
annotate
|
| Sun, 08 Sep 2019 17:49:35 +0200 |
wenzelm |
clarified syntax: 'directories' and 'theories' belong together;
|
file |
diff |
annotate
|
| Sun, 08 Sep 2019 16:49:05 +0200 |
wenzelm |
declare session directories;
|
file |
diff |
annotate
|
| Sat, 07 Sep 2019 12:16:11 +0200 |
wenzelm |
avoid overlapping session directories;
|
file |
diff |
annotate
|
| Fri, 06 Sep 2019 15:50:57 +0200 |
wenzelm |
proper session-qualifier imports (amending "fixes" from adaa0a6ea4fe);
|
file |
diff |
annotate
|
| Tue, 03 Sep 2019 14:58:29 +0200 |
wenzelm |
more dump_checkpoints;
|
file |
diff |
annotate
|
| Thu, 29 Aug 2019 17:13:49 +0200 |
wenzelm |
more scalable isabelle dump (and derivatives): mark individual theories to share common data in ML;
|
file |
diff |
annotate
|
| Tue, 13 Aug 2019 20:54:08 +0200 |
wenzelm |
NEWS and example for Theory.join_theory;
|
file |
diff |
annotate
|
| Tue, 23 Jul 2019 12:07:50 +0200 |
wenzelm |
proof terms are always constructed sequentially;
|
file |
diff |
annotate
|
| Thu, 09 May 2019 12:32:47 +0200 |
nipkow |
New version of tries
|
file |
diff |
annotate
|
| Tue, 16 Apr 2019 19:50:19 +0000 |
haftmann |
entry point for comprehensive word library
|
file |
diff |
annotate
|
| Tue, 16 Apr 2019 19:50:18 +0000 |
haftmann |
tuned theory names
|
file |
diff |
annotate
|
| Tue, 16 Apr 2019 19:50:09 +0000 |
haftmann |
integrated Bit_Comparison into Word corpus
|
file |
diff |
annotate
|
| Sat, 13 Apr 2019 16:33:33 +0200 |
wenzelm |
clarified group of "main" library sessions;
|
file |
diff |
annotate
|
| Tue, 09 Apr 2019 15:30:58 +0100 |
paulson |
new Homology target, depending on HOL-Algebra and HOL-Analysis
|
file |
diff |
annotate
|
| Mon, 08 Apr 2019 15:26:54 +0100 |
paulson |
First tranche of the Homology development: Simplices
|
file |
diff |
annotate
|
| Sun, 07 Apr 2019 08:26:57 +0200 |
traytel |
bundle for cardinal syntax
|
file |
diff |
annotate
|
| Tue, 02 Apr 2019 13:22:16 +0200 |
wenzelm |
more convenient export;
|
file |
diff |
annotate
|
| Sat, 30 Mar 2019 15:37:27 +0100 |
haftmann |
experimental commands for proof sketching and exploration
|
file |
diff |
annotate
|
| Wed, 20 Mar 2019 20:15:30 +0100 |
wenzelm |
access OCaml tools and libraries via ISABELLE_OCAMLFIND;
|
file |
diff |
annotate
|
| Fri, 14 Dec 2018 14:33:26 +0100 |
Manuel Eberl |
Added triangular numbers
|
file |
diff |
annotate
|
| Fri, 18 Jan 2019 19:48:04 -0500 |
immler |
automation for unverloading definitions
|
file |
diff |
annotate
|
| Sun, 30 Dec 2018 10:34:56 +0000 |
haftmann |
redundant
|
file |
diff |
annotate
|
| Fri, 28 Dec 2018 18:53:19 +0100 |
nipkow |
tuned headers etc, added bib-file
|
file |
diff |
annotate
|
| Tue, 20 Nov 2018 13:46:13 +0100 |
wenzelm |
tuned -- refining auto-update 15e9ed5b28fb;
|
file |
diff |
annotate
|
| Thu, 08 Nov 2018 22:29:09 +0100 |
wenzelm |
isabelle update_cartouches -t;
|
file |
diff |
annotate
|
| Wed, 07 Nov 2018 11:08:12 +0000 |
haftmann |
dedicated examples for sorting
|
file |
diff |
annotate
|
| Wed, 17 Oct 2018 21:00:53 +0200 |
nipkow |
added Array files
|
file |
diff |
annotate
|
| Sun, 07 Oct 2018 16:28:38 +0200 |
nipkow |
added Braun_Tree.thy
|
file |
diff |
annotate
|
| Mon, 01 Oct 2018 12:41:35 +0200 |
wenzelm |
HOL-SPARK .prv files are no longer written to the file-system;
|
file |
diff |
annotate
|
| Sun, 30 Sep 2018 13:00:08 +0200 |
wenzelm |
de-emphasize HOL-SPARK: somewhat outdated;
|
file |
diff |
annotate
|
| Wed, 05 Sep 2018 05:05:00 +0200 |
nipkow |
tuned doc
|
file |
diff |
annotate
|
| Sat, 28 Jul 2018 16:49:53 +0200 |
wenzelm |
more robust: potentially a workaround for spurious HOL build problems seen by Larry Paulson;
|
file |
diff |
annotate
|
| Sun, 22 Jul 2018 19:29:51 +0200 |
eberlm |
Moved Real_Asymp manual
|
file |
diff |
annotate
|
| Wed, 18 Jul 2018 16:44:01 +0200 |
wenzelm |
prefer HTTPS;
|
file |
diff |
annotate
|
| Sun, 15 Jul 2018 23:44:52 +0200 |
Andreas Lochbihler |
merged
|
file |
diff |
annotate
|
| Sun, 15 Jul 2018 23:44:38 +0200 |
Andreas Lochbihler |
more examples for Code_Lazy
|
file |
diff |
annotate
|
| Sun, 15 Jul 2018 14:46:57 +0200 |
Manuel Eberl |
Added Real_Asymp package
|
file |
diff |
annotate
|
| Thu, 12 Jul 2018 11:23:46 +0200 |
nipkow |
more economic tagging
|
file |
diff |
annotate
|
| Tue, 10 Jul 2018 09:38:35 +0200 |
immler |
make theorem, corollary, and proposition %important for HOL-Analysis manual
|
file |
diff |
annotate
|
| Mon, 02 Jul 2018 14:41:35 +0100 |
paulson |
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
|
file |
diff |
annotate
|
| Wed, 27 Jun 2018 11:16:43 +0200 |
immler |
example for Types_To_Sets: transfer from type-based linear algebra to subspaces
|
file |
diff |
annotate
|
| Tue, 26 Jun 2018 22:39:06 +0200 |
nipkow |
new theory Trie
|
file |
diff |
annotate
|
| Tue, 26 Jun 2018 19:03:13 +0200 |
wenzelm |
clarified syntax;
|
file |
diff |
annotate
|
| Tue, 26 Jun 2018 17:42:49 +0200 |
wenzelm |
simplified: allow only command names, with dummy for default;
|
file |
diff |
annotate
|
| 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
|