| Sat, 13 Sep 2025 17:47:57 +0200 |
wenzelm |
avoid significant slowdown of HOL-ex and HOL-Codegenerator_Test (amending 7d6e6531de61);
|
file |
diff |
annotate
|
| Sun, 07 Sep 2025 22:37:57 +0100 |
paulson |
Removing "HOL-Library" as ancestor theory
|
file |
diff |
annotate
|
| Thu, 07 Aug 2025 20:33:28 +0200 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Fri, 18 Apr 2025 12:33:01 +0200 |
Manuel Eberl |
added orphaned theory to HOL-Analysis
|
file |
diff |
annotate
|
| Sun, 16 Mar 2025 08:55:17 +0100 |
haftmann |
removed theory HOL-Library.Divides (finally)
|
file |
diff |
annotate
|
| Sun, 09 Feb 2025 11:14:59 +0100 |
haftmann |
streamlined and actually integrated
|
file |
diff |
annotate
|
| Thu, 06 Feb 2025 17:28:27 +0100 |
nipkow |
added Example theory
|
file |
diff |
annotate
|
| Tue, 28 Jan 2025 21:42:51 +0100 |
haftmann |
clarifed terminology
|
file |
diff |
annotate
|
| Tue, 28 Jan 2025 13:02:42 +0100 |
haftmann |
more explicit tests for non-PolyML SML platforms
|
file |
diff |
annotate
|
| Mon, 27 Jan 2025 12:13:37 +0100 |
wenzelm |
move theory "HOL-Library.Adhoc_Overloading" to Pure;
|
file |
diff |
annotate
|
| Mon, 20 Jan 2025 22:15:11 +0100 |
haftmann |
systematic checks for bit operations and more rules on symbolic terms
|
file |
diff |
annotate
|
| Fri, 17 Jan 2025 23:10:39 +0100 |
wenzelm |
proper condition for strict "test_code check in OCaml" and "test_code check in GHC";
|
file |
diff |
annotate
|
| Wed, 15 Jan 2025 16:45:12 +0100 |
nipkow |
Compact notation for Suc numerals.
|
file |
diff |
annotate
|
| Fri, 10 Jan 2025 18:35:46 +0100 |
haftmann |
more correct code generation for string literals
|
file |
diff |
annotate
|
| Sat, 04 Jan 2025 17:38:45 +0100 |
haftmann |
separate theory for tests checking bit operations
|
file |
diff |
annotate
|
| Thu, 05 Dec 2024 19:44:53 +0100 |
nipkow |
added Halting problem theory
|
file |
diff |
annotate
|
| 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
|