src/HOL/ROOT
Sat, 07 Sep 2019 12:16:11 +0200 wenzelm avoid overlapping session directories;
Fri, 06 Sep 2019 15:50:57 +0200 wenzelm proper session-qualifier imports (amending "fixes" from adaa0a6ea4fe);
Tue, 03 Sep 2019 14:58:29 +0200 wenzelm more dump_checkpoints;
Thu, 29 Aug 2019 17:13:49 +0200 wenzelm more scalable isabelle dump (and derivatives): mark individual theories to share common data in ML;
Tue, 13 Aug 2019 20:54:08 +0200 wenzelm NEWS and example for Theory.join_theory;
Tue, 23 Jul 2019 12:07:50 +0200 wenzelm proof terms are always constructed sequentially;
Thu, 09 May 2019 12:32:47 +0200 nipkow New version of tries
Tue, 16 Apr 2019 19:50:19 +0000 haftmann entry point for comprehensive word library
Tue, 16 Apr 2019 19:50:18 +0000 haftmann tuned theory names
Tue, 16 Apr 2019 19:50:09 +0000 haftmann integrated Bit_Comparison into Word corpus
Sat, 13 Apr 2019 16:33:33 +0200 wenzelm clarified group of "main" library sessions;
Tue, 09 Apr 2019 15:30:58 +0100 paulson new Homology target, depending on HOL-Algebra and HOL-Analysis
Mon, 08 Apr 2019 15:26:54 +0100 paulson First tranche of the Homology development: Simplices draft
Sun, 07 Apr 2019 08:26:57 +0200 traytel bundle for cardinal syntax draft
Tue, 02 Apr 2019 13:22:16 +0200 wenzelm more convenient export;
Sat, 30 Mar 2019 15:37:27 +0100 haftmann experimental commands for proof sketching and exploration
Wed, 20 Mar 2019 20:15:30 +0100 wenzelm access OCaml tools and libraries via ISABELLE_OCAMLFIND;
Fri, 14 Dec 2018 14:33:26 +0100 Manuel Eberl Added triangular numbers draft
Fri, 18 Jan 2019 19:48:04 -0500 immler automation for unverloading definitions
Sun, 30 Dec 2018 10:34:56 +0000 haftmann redundant
Fri, 28 Dec 2018 18:53:19 +0100 nipkow tuned headers etc, added bib-file
Fri, 14 Dec 2018 14:33:26 +0100 Manuel Eberl Added triangular numbers draft
Tue, 20 Nov 2018 13:46:13 +0100 wenzelm tuned -- refining auto-update 15e9ed5b28fb;
Thu, 08 Nov 2018 22:29:09 +0100 wenzelm isabelle update_cartouches -t;
Wed, 07 Nov 2018 11:08:12 +0000 haftmann dedicated examples for sorting
Wed, 17 Oct 2018 21:00:53 +0200 nipkow added Array files
Sun, 07 Oct 2018 16:28:38 +0200 nipkow added Braun_Tree.thy
Mon, 01 Oct 2018 12:41:35 +0200 wenzelm HOL-SPARK .prv files are no longer written to the file-system;
Sun, 30 Sep 2018 13:00:08 +0200 wenzelm de-emphasize HOL-SPARK: somewhat outdated;
Wed, 05 Sep 2018 05:05:00 +0200 nipkow tuned doc
Sat, 28 Jul 2018 16:49:53 +0200 wenzelm more robust: potentially a workaround for spurious HOL build problems seen by Larry Paulson;
Sun, 22 Jul 2018 19:29:51 +0200 eberlm Moved Real_Asymp manual
Wed, 18 Jul 2018 16:44:01 +0200 wenzelm prefer HTTPS;
Sun, 15 Jul 2018 23:44:52 +0200 Andreas Lochbihler merged
Sun, 15 Jul 2018 23:44:38 +0200 Andreas Lochbihler more examples for Code_Lazy
Sun, 15 Jul 2018 14:46:57 +0200 Manuel Eberl Added Real_Asymp package
Thu, 12 Jul 2018 11:23:46 +0200 nipkow more economic tagging
Tue, 10 Jul 2018 09:38:35 +0200 immler make theorem, corollary, and proposition %important for HOL-Analysis manual
Mon, 02 Jul 2018 14:41:35 +0100 paulson Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
Wed, 27 Jun 2018 11:16:43 +0200 immler example for Types_To_Sets: transfer from type-based linear algebra to subspaces
Tue, 26 Jun 2018 22:39:06 +0200 nipkow new theory Trie
Tue, 26 Jun 2018 19:03:13 +0200 wenzelm clarified syntax;
Tue, 26 Jun 2018 17:42:49 +0200 wenzelm simplified: allow only command names, with dummy for default;
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
Tue, 12 Jun 2018 16:08:57 +0100 paulson New material from Martin Baillon and Paulo Emílio de Vilhena
Tue, 29 May 2018 14:05:59 +0200 nipkow canonical names
Thu, 24 May 2018 14:42:47 +0200 nipkow reorganization, everything based on Tree2 now
Sat, 12 May 2018 11:24:11 +0200 Andreas Lochbihler new tool Code_Lazy
Wed, 09 May 2018 22:25:24 +0200 wenzelm less ambitious parallelism, notably for threads=2;
Wed, 25 Apr 2018 13:29:21 +0000 haftmann proof of concept for residue rings over int using type numerals
Tue, 24 Apr 2018 14:17:58 +0000 haftmann proper datatype for 8-bit characters
Sun, 08 Apr 2018 11:05:52 +0200 nipkow more name tuning
Wed, 21 Mar 2018 20:17:25 +0100 haftmann proof of concept for algebraically founded bit lists
Wed, 14 Feb 2018 16:32:09 +0100 nipkow New theory ex/Radix_Sort.thy
Wed, 14 Feb 2018 11:51:03 +0100 Lars Hupel records based on datatypes/BNF infrastructure
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
Sun, 24 Dec 2017 14:28:10 +0100 eberlm Removed Analysis/ex/Circle_Area; replaced by more general Analysis/Ball_Volume
Mon, 18 Dec 2017 16:58:13 +0100 traytel a conditional paramitrecity prover
Sat, 16 Dec 2017 16:46:01 +0100 wenzelm PIDE markup for session ROOT files;
Thu, 07 Dec 2017 20:55:03 +0100 wenzelm more robust;
less more (0) -300 -100 -60 tip