src/HOL/ROOT
Fri, 16 Oct 2020 19:34:37 +0200 Mathias Fleury reactivate veriT after changing options in 11f645d25498
Thu, 15 Oct 2020 13:24:16 +0200 wenzelm proper Isabelle component settings: prefer standard terminology "ISABELLE_VERIT", avoid conflict of "VERIT_VERSION" with processing of implicit options by veriT;
Mon, 12 Oct 2020 18:59:44 +0200 Mathias Fleury add reconstruction for the SMT solver veriT
Wed, 07 Oct 2020 17:34:24 +0200 nipkow Aded Queues
Tue, 29 Sep 2020 12:12:34 +0200 wenzelm clarified default (see also 0c7a74a1c6d9);
Sat, 26 Sep 2020 17:04:51 +0200 wenzelm less bulky session stack;
Thu, 17 Sep 2020 09:57:31 +0000 haftmann integrated generic conversions into word corpse
Tue, 25 Aug 2020 15:02:56 +0200 wenzelm test HOL-Nitpick_Examples with Isabelle/Scala instead of external process: much faster;
Mon, 24 Aug 2020 13:39:09 +0000 haftmann a proof of concept for generic conversions
Sat, 22 Aug 2020 13:55:42 +0200 wenzelm clarified session: no parent image for minor theory imports;
Thu, 06 Aug 2020 15:37:14 +0000 haftmann tailored towards remaining essence
Thu, 06 Aug 2020 17:11:33 +0200 nipkow added theory Tree23_of_List
Fri, 17 Jul 2020 17:06:54 +0200 wenzelm proper session imports;
Thu, 16 Jul 2020 16:53:08 +0200 wenzelm proper import sessions;
Mon, 13 Jul 2020 17:08:45 +0200 wenzelm clarified examples;
Thu, 02 Jul 2020 12:10:58 +0000 haftmann extraction of equations x = t from premises beneath meta-all
Tue, 09 Jun 2020 12:13:15 +0100 paulson New Ackermann development
Mon, 08 Jun 2020 21:55:14 +0200 wenzelm clarified sessions;
Mon, 08 Jun 2020 21:38:41 +0200 wenzelm clarified sessions: "Notable Examples in Isabelle/HOL";
Mon, 08 Jun 2020 15:09:57 +0200 wenzelm clarified sessions: "Notable Examples in Isabelle/Pure";
Sun, 17 May 2020 17:18:32 +0200 nipkow another AVL tree version
Mon, 04 May 2020 17:35:29 +0200 Manuel Eberl New HOL simproc 'datatype_no_proper_subterm'
Tue, 12 May 2020 16:29:26 +0200 wenzelm clarified session imports: avoid bulky HOL-Library image;
Mon, 04 May 2020 16:28:39 +0200 nipkow AVL trees with balance tags
Sat, 25 Apr 2020 16:31:43 +0200 nipkow added Height_Balanced_Trees
Fri, 17 Apr 2020 20:55:53 +0100 paulson New theory Library/List_Lenlexorder.thy, a type class instantiation for well-ordering lists
Tue, 03 Mar 2020 19:26:24 +0000 haftmann library theory for extractions of equations x = t into premises
Fri, 28 Feb 2020 21:23:11 +0100 traytel tuned lift_bnf's user interface for quotients
Mon, 03 Feb 2020 16:49:44 +0100 nipkow added Interval_Tree.thy
Sun, 19 Jan 2020 07:50:35 +0100 traytel new examples of BNF lifting across quotients using a new theory of confluence,
Tue, 07 Jan 2020 12:37:12 +0100 nipkow alternative deletion in Red-Black trees
Tue, 10 Dec 2019 01:06:39 +0100 traytel an extensive example for lift_bnf across quotients
Sat, 30 Nov 2019 13:47:33 +0100 Manuel Eberl Split off new HOL-Complex_Analysis session from HOL-Analysis
Mon, 04 Nov 2019 20:38:15 +0000 haftmann proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
Sun, 27 Oct 2019 20:53:10 -0400 immler a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
Sun, 27 Oct 2019 20:07:59 -0400 immler added examples for "metric" method, by Maximilian Schäffeler
Sun, 13 Oct 2019 16:26:31 +0200 wenzelm clarified sessions/directories;
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;
Wed, 02 Oct 2019 20:58:09 +0200 wenzelm just one dump_checkpoint Main -- potentially more robust;
Sun, 08 Sep 2019 17:49:35 +0200 wenzelm clarified syntax: 'directories' and 'theories' belong together;
Sun, 08 Sep 2019 16:49:05 +0200 wenzelm declare session directories;
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
Sun, 07 Apr 2019 08:26:57 +0200 traytel bundle for cardinal syntax
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
Fri, 18 Jan 2019 19:48:04 -0500 immler automation for unverloading definitions
less more (0) -300 -100 -60 tip