| Thu, 15 Aug 2024 13:58:09 +0200 |
wenzelm |
adapt and activate congprocs examples, following the current Simplifier implementation;
|
file |
diff |
annotate
|
| Sun, 30 Jun 2024 06:30:08 +0000 |
haftmann |
moved transitional theory Divides to HOL-Library
|
file |
diff |
annotate
|
| Tue, 25 Jun 2024 11:08:00 +0200 |
nipkow |
clarified ternary tries
|
file |
diff |
annotate
|
| Thu, 04 Apr 2024 15:29:41 +0200 |
Manuel Eberl |
moved over material from the AFP to HOL, HOL-Computational_Algebra, and HOL-Number_Theory
|
file |
diff |
annotate
|
| Fri, 29 Mar 2024 19:28:59 +0100 |
Manuel Eberl |
moved over material from AFP; most importantly on algebraic numbers and algebraically closed fields
|
file |
diff |
annotate
|
| Fri, 03 Nov 2023 16:20:06 +0000 |
paulson |
Added Kronecker's approximation theorem. Requires adding Real_Asymp to HOL-Analysis. Funny syntax issue in Probability/Projective_Family
|
file |
diff |
annotate
|
| Wed, 20 Sep 2023 17:40:09 +0200 |
desharna |
added first proof reconstruction test for Sledgehammer
|
file |
diff |
annotate
|
| Sun, 06 Aug 2023 14:48:25 +0200 |
wenzelm |
no hardwired timeout in Isabelle distribution (unlike on AFP): reverting part of 74c75da4cb01 -- without further tinkering it breaks isabelle_cronjob builds;
|
file |
diff |
annotate
|
| Wed, 12 Jul 2023 22:28:38 +0100 |
paulson |
Doubled the time limit for HOL-Probability
|
file |
diff |
annotate
|
| Wed, 12 Jul 2023 18:28:11 +0100 |
paulson |
Some fixes, and SOME TIME LIMITS
|
file |
diff |
annotate
|
| Fri, 30 Jun 2023 13:12:10 +0200 |
nipkow |
New theory Leftist_Heap_List
|
file |
diff |
annotate
|
| Wed, 08 Mar 2023 08:10:10 +0100 |
nipkow |
new theory Tree_Rotations
|
file |
diff |
annotate
|
| Fri, 20 Jan 2023 22:47:55 +0100 |
wenzelm |
more correct and complete bibliography;
|
file |
diff |
annotate
|
| Thu, 19 Jan 2023 13:55:38 +0000 |
paulson |
HOL/Library/BigO is obsolete
|
file |
diff |
annotate
|
| Thu, 25 Aug 2022 21:42:21 +0100 |
paulson |
Removal of a duplicate theory, since that material and more is in the AFP: https://www.isa-afp.org/entries/Bernoulli.html
|
file |
diff |
annotate
|
| Sun, 21 Aug 2022 14:01:59 +0000 |
haftmann |
Gauss numbers
|
file |
diff |
annotate
|
| Sun, 21 Aug 2022 06:18:23 +0000 |
haftmann |
streamlined
|
file |
diff |
annotate
|
| Fri, 19 Aug 2022 23:58:44 +0200 |
wenzelm |
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
|
file |
diff |
annotate
|
| Mon, 04 Jul 2022 07:57:22 +0000 |
haftmann |
officical abstract characters for code generation
|
file |
diff |
annotate
|
| Thu, 24 Mar 2022 18:50:11 +0000 |
paulson |
really removing Dedekind_real
|
file |
diff |
annotate
|
| Wed, 23 Mar 2022 14:36:11 +0000 |
paulson |
... and removing Primrec from ROOT too
|
file |
diff |
annotate
|
| Thu, 09 Dec 2021 08:32:29 +0100 |
nipkow |
Rewrite: added links to docu, made more prominent
|
file |
diff |
annotate
|
| Wed, 06 Oct 2021 14:19:46 +0200 |
eberlm |
new notion of infinite sums in HOL-Analysis, ordering on complex numbers
|
file |
diff |
annotate
|
| Sun, 26 Sep 2021 18:49:55 +0200 |
wenzelm |
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
|
file |
diff |
annotate
|
| Fri, 10 Sep 2021 21:55:55 +0200 |
wenzelm |
tuned comments;
|
file |
diff |
annotate
|
| Wed, 25 Aug 2021 22:10:15 +0200 |
nipkow |
reflect moved theories
|
file |
diff |
annotate
|
| Tue, 03 Aug 2021 13:53:22 +0000 |
haftmann |
obsolete
|
file |
diff |
annotate
|
| Sun, 06 Jun 2021 21:17:23 +0200 |
wenzelm |
suppress theories from other sessions, unless explicitly specified via mirabelle_theories;
|
file |
diff |
annotate
|
| Sat, 05 Jun 2021 12:57:52 +0200 |
wenzelm |
clarified examples;
|
file |
diff |
annotate
|
| Fri, 14 May 2021 21:32:11 +0200 |
wenzelm |
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
|
file |
diff |
annotate
|
| Mon, 10 May 2021 19:45:51 +0000 |
haftmann |
guide is out of focus
|
file |
diff |
annotate
|
| Mon, 10 May 2021 17:15:37 +0200 |
wenzelm |
proper settings variable, amending 6e85281177df;
|
file |
diff |
annotate
|
| Mon, 10 May 2021 14:28:37 +0200 |
wenzelm |
proper condition: z3 could be absent, e.g. on arm64-linux;
|
file |
diff |
annotate
|
| Thu, 08 Apr 2021 12:38:18 +0000 |
haftmann |
confluent preprocessing for floats in presence of target language numerals
|
file |
diff |
annotate
|
| Thu, 25 Mar 2021 08:52:15 +0000 |
haftmann |
dedicated session for combinatorial material
|
file |
diff |
annotate
|
| Thu, 11 Mar 2021 10:25:04 +0100 |
traytel |
another example for lift_bnf for quotients
|
file |
diff |
annotate
|
| Tue, 09 Mar 2021 14:20:27 +0100 |
traytel |
generalized confluence-based subdistributivity theorem for quotients;
|
file |
diff |
annotate
|
| Fri, 08 Jan 2021 19:53:44 +0100 |
Manuel Eberl |
HOL-Data_Structures: added Selection and time functions for list functions
|
file |
diff |
annotate
|
| Wed, 23 Dec 2020 23:19:09 +0100 |
wenzelm |
more robust defaults: spurious problems with parallel invocations and interrupts;
|
file |
diff |
annotate
|
| Wed, 23 Dec 2020 20:49:05 +0100 |
wenzelm |
clarified session: avoid merge of different syntax from different Hoare logics;
|
file |
diff |
annotate
|
| Wed, 23 Dec 2020 17:16:05 +0100 |
wenzelm |
clarified modules: avoid multiple uses of the same ML file;
|
file |
diff |
annotate
|
| Mon, 07 Dec 2020 22:28:41 +0100 |
wenzelm |
spelling;
|
file |
diff |
annotate
|
| Sun, 06 Dec 2020 13:49:25 +0100 |
wenzelm |
more Unicode;
|
file |
diff |
annotate
|
| Sun, 06 Dec 2020 13:44:07 +0100 |
wenzelm |
eliminated odd "Read_me";
|
file |
diff |
annotate
|
| Sun, 06 Dec 2020 13:31:42 +0100 |
wenzelm |
eliminated odd "Read_me";
|
file |
diff |
annotate
|
| Mon, 23 Nov 2020 19:57:55 +0100 |
nipkow |
proper defn of a heap
|
file |
diff |
annotate
|
| Mon, 16 Nov 2020 22:21:40 +0100 |
wenzelm |
clarified document;
|
file |
diff |
annotate
|
| Sat, 14 Nov 2020 12:57:28 +0100 |
wenzelm |
proper document_theories;
|
file |
diff |
annotate
|
| Sun, 01 Nov 2020 16:54:49 +0100 |
haftmann |
bundle mixins for locale and class specifications
|
file |
diff |
annotate
|
| Thu, 29 Oct 2020 10:03:03 +0000 |
haftmann |
moved most material from session HOL-Word to Word_Lib in the AFP
|
file |
diff |
annotate
|
| Fri, 16 Oct 2020 19:34:37 +0200 |
Mathias Fleury |
reactivate veriT after changing options in 11f645d25498
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Mon, 12 Oct 2020 18:59:44 +0200 |
Mathias Fleury |
add reconstruction for the SMT solver veriT
|
file |
diff |
annotate
|
| Wed, 07 Oct 2020 17:34:24 +0200 |
nipkow |
Aded Queues
|
file |
diff |
annotate
|
| Tue, 29 Sep 2020 12:12:34 +0200 |
wenzelm |
clarified default (see also 0c7a74a1c6d9);
|
file |
diff |
annotate
|
| Sat, 26 Sep 2020 17:04:51 +0200 |
wenzelm |
less bulky session stack;
|
file |
diff |
annotate
|
| Thu, 17 Sep 2020 09:57:31 +0000 |
haftmann |
integrated generic conversions into word corpse
|
file |
diff |
annotate
|
| Tue, 25 Aug 2020 15:02:56 +0200 |
wenzelm |
test HOL-Nitpick_Examples with Isabelle/Scala instead of external process: much faster;
|
file |
diff |
annotate
|
| Mon, 24 Aug 2020 13:39:09 +0000 |
haftmann |
a proof of concept for generic conversions
|
file |
diff |
annotate
|
| Sat, 22 Aug 2020 13:55:42 +0200 |
wenzelm |
clarified session: no parent image for minor theory imports;
|
file |
diff |
annotate
|
| Thu, 06 Aug 2020 15:37:14 +0000 |
haftmann |
tailored towards remaining essence
|
file |
diff |
annotate
|
| Thu, 06 Aug 2020 17:11:33 +0200 |
nipkow |
added theory Tree23_of_List
|
file |
diff |
annotate
|
| Fri, 17 Jul 2020 17:06:54 +0200 |
wenzelm |
proper session imports;
|
file |
diff |
annotate
|
| Thu, 16 Jul 2020 16:53:08 +0200 |
wenzelm |
proper import sessions;
|
file |
diff |
annotate
|
| Mon, 13 Jul 2020 17:08:45 +0200 |
wenzelm |
clarified examples;
|
file |
diff |
annotate
|
| Thu, 02 Jul 2020 12:10:58 +0000 |
haftmann |
extraction of equations x = t from premises beneath meta-all
|
file |
diff |
annotate
|
| Tue, 09 Jun 2020 12:13:15 +0100 |
paulson |
New Ackermann development
|
file |
diff |
annotate
|
| Mon, 08 Jun 2020 21:55:14 +0200 |
wenzelm |
clarified sessions;
|
file |
diff |
annotate
|
| Mon, 08 Jun 2020 21:38:41 +0200 |
wenzelm |
clarified sessions: "Notable Examples in Isabelle/HOL";
|
file |
diff |
annotate
|
| Mon, 08 Jun 2020 15:09:57 +0200 |
wenzelm |
clarified sessions: "Notable Examples in Isabelle/Pure";
|
file |
diff |
annotate
|
| Sun, 17 May 2020 17:18:32 +0200 |
nipkow |
another AVL tree version
|
file |
diff |
annotate
|
| Mon, 04 May 2020 17:35:29 +0200 |
Manuel Eberl |
New HOL simproc 'datatype_no_proper_subterm'
|
file |
diff |
annotate
|
| Tue, 12 May 2020 16:29:26 +0200 |
wenzelm |
clarified session imports: avoid bulky HOL-Library image;
|
file |
diff |
annotate
|
| Mon, 04 May 2020 16:28:39 +0200 |
nipkow |
AVL trees with balance tags
|
file |
diff |
annotate
|
| Sat, 25 Apr 2020 16:31:43 +0200 |
nipkow |
added Height_Balanced_Trees
|
file |
diff |
annotate
|
| Fri, 17 Apr 2020 20:55:53 +0100 |
paulson |
New theory Library/List_Lenlexorder.thy, a type class instantiation for well-ordering lists
|
file |
diff |
annotate
|
| Tue, 03 Mar 2020 19:26:24 +0000 |
haftmann |
library theory for extractions of equations x = t into premises
|
file |
diff |
annotate
|
| Fri, 28 Feb 2020 21:23:11 +0100 |
traytel |
tuned lift_bnf's user interface for quotients
|
file |
diff |
annotate
|
| Mon, 03 Feb 2020 16:49:44 +0100 |
nipkow |
added Interval_Tree.thy
|
file |
diff |
annotate
|
| Sun, 19 Jan 2020 07:50:35 +0100 |
traytel |
new examples of BNF lifting across quotients using a new theory of confluence,
|
file |
diff |
annotate
|
| Tue, 07 Jan 2020 12:37:12 +0100 |
nipkow |
alternative deletion in Red-Black trees
|
file |
diff |
annotate
|
| Tue, 10 Dec 2019 01:06:39 +0100 |
traytel |
an extensive example for lift_bnf across quotients
|
file |
diff |
annotate
|
| Sat, 30 Nov 2019 13:47:33 +0100 |
Manuel Eberl |
Split off new HOL-Complex_Analysis session from HOL-Analysis
|
file |
diff |
annotate
|
| 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
|
file |
diff |
annotate
|
| Sun, 27 Oct 2019 20:53:10 -0400 |
immler |
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
|
file |
diff |
annotate
|
| Sun, 27 Oct 2019 20:07:59 -0400 |
immler |
added examples for "metric" method, by Maximilian Schäffeler
|
file |
diff |
annotate
|
| 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
|