| Fri, 31 Jan 2025 17:01:27 +0100 |
Lukas Stevens |
more canonical formatting
|
changeset |
files
|
| Fri, 31 Jan 2025 16:59:12 +0100 |
Lukas Stevens |
add hook to insert premises in the order solver
|
changeset |
files
|
| Fri, 31 Jan 2025 16:23:53 +0100 |
wenzelm |
less NEWS (see also afae60d6ff15);
|
changeset |
files
|
| Wed, 08 Jan 2025 15:19:37 +0100 |
wenzelm |
switch from CVC5 to cvc5, including updates of internal tool references;
|
changeset |
files
|
| Thu, 30 Jan 2025 22:29:45 +0100 |
wenzelm |
more robust wrt. Par_List.map in Browser_Info.build(), see also 2fff9ce6b460 and 787a203a20b6;
|
changeset |
files
|
| Thu, 30 Jan 2025 21:44:44 +0100 |
wenzelm |
more thorough cleanup;
|
changeset |
files
|
| Thu, 30 Jan 2025 20:55:42 +0100 |
wenzelm |
more options for build_release: support bundled browser_info and Find_Facts database;
|
changeset |
files
|
| Thu, 30 Jan 2025 13:16:51 +0100 |
wenzelm |
more standard directory structure;
|
changeset |
files
|
| Thu, 30 Jan 2025 13:13:21 +0100 |
wenzelm |
tuned output;
|
changeset |
files
|
| Thu, 30 Jan 2025 11:53:26 +0100 |
wenzelm |
suppress MacOS.jar from jEdit 5.7.0, following 65fd0f032a75;
|
changeset |
files
|
| Wed, 29 Jan 2025 21:25:44 +0100 |
wenzelm |
tuned GUI: attempt to improve divider mobility;
|
changeset |
files
|
| Wed, 29 Jan 2025 20:52:27 +0100 |
wenzelm |
rebuild jedit component;
|
changeset |
files
|
| Wed, 29 Jan 2025 20:17:21 +0100 |
wenzelm |
make double sure that buffer.lineSeparator is well-defined: prevent a situation where $JEDIT_SETTINGS/properties would contain "buffer.lineSeparator=" and new-file would lead to a buffer with empty lineSeparator, and save would produce just one line;
|
changeset |
files
|
| Wed, 29 Jan 2025 14:43:14 +0100 |
wenzelm |
more accurate syntax: follow documentation in "isar-ref" (and command 'syntax_consts');
|
changeset |
files
|
| Wed, 29 Jan 2025 11:53:49 +0100 |
wenzelm |
more robust: make double sure that buffer.getText() is valid (see also 2e7073976c25);
|
changeset |
files
|
| Tue, 28 Jan 2025 21:42:51 +0100 |
haftmann |
clarifed terminology
|
changeset |
files
|
| Tue, 28 Jan 2025 21:42:04 +0100 |
nipkow |
extracted the ^^ subtheory for modularity reasons
|
changeset |
files
|
| Tue, 28 Jan 2025 17:30:00 +0100 |
nipkow |
tuned
|
changeset |
files
|
| Tue, 28 Jan 2025 14:53:36 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Tue, 28 Jan 2025 14:53:08 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 28 Jan 2025 13:42:40 +0100 |
wenzelm |
minor performance tuning;
|
changeset |
files
|
| Tue, 28 Jan 2025 13:37:02 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 28 Jan 2025 13:35:08 +0100 |
wenzelm |
tuned names;
|
changeset |
files
|
| Tue, 28 Jan 2025 13:33:07 +0100 |
wenzelm |
minor performance tuning: avoid somewhat indirect filter / add_consts;
|
changeset |
files
|
| Tue, 28 Jan 2025 11:29:42 +0100 |
wenzelm |
clarified signature: more standard map_data;
|
changeset |
files
|
| Tue, 28 Jan 2025 11:20:53 +0100 |
wenzelm |
misc tuning;
|
changeset |
files
|
| Tue, 28 Jan 2025 11:17:07 +0100 |
wenzelm |
clarified signature with minor performance tuning: avoid Context.proof_of with its Proof_Context.init_global;
|
changeset |
files
|
| Tue, 28 Jan 2025 11:05:45 +0100 |
wenzelm |
tuned names;
|
changeset |
files
|
| Tue, 28 Jan 2025 13:02:42 +0100 |
haftmann |
more explicit tests for non-PolyML SML platforms
|
changeset |
files
|
| Tue, 28 Jan 2025 07:17:30 +0100 |
haftmann |
typo
|
changeset |
files
|
| Mon, 27 Jan 2025 22:27:18 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Mon, 27 Jan 2025 21:31:11 +0100 |
wenzelm |
more NEWS;
|
changeset |
files
|
| Mon, 27 Jan 2025 21:31:02 +0100 |
wenzelm |
clarified syntax;
|
changeset |
files
|
| Mon, 27 Jan 2025 20:29:02 +0100 |
wenzelm |
support for "no" polarity of 'adhoc_overloading' vs. 'no_adhoc_overloading';
|
changeset |
files
|
| Mon, 27 Jan 2025 18:32:18 +0100 |
wenzelm |
more operations;
|
changeset |
files
|
| Mon, 27 Jan 2025 14:14:30 +0100 |
wenzelm |
clarified signature: proper ML interface to main command, without exposing too many internals;
|
changeset |
files
|
| Mon, 27 Jan 2025 12:52:19 +0100 |
wenzelm |
tuned signature: more explicit Type.raw_equiv;
|
changeset |
files
|
| Mon, 27 Jan 2025 12:24:51 +0100 |
wenzelm |
more liberal type equivalence, following thys/Transport/HOL_Basics/Adhoc_Overloading/Adhoc_Overloading.thy from AFP/e69d71bc07c4;
|
changeset |
files
|
| Mon, 27 Jan 2025 12:13:37 +0100 |
wenzelm |
move theory "HOL-Library.Adhoc_Overloading" to Pure;
|
changeset |
files
|
| Sun, 26 Jan 2025 22:45:57 +0100 |
wenzelm |
discontinue odd "-build" suffix altogether (see also f51b0b54b20b, bec95e287d26, 6b45a1568637);
|
changeset |
files
|
| Mon, 27 Jan 2025 13:13:30 +0100 |
haftmann |
more frugal exports
|
changeset |
files
|
| Mon, 27 Jan 2025 13:13:28 +0100 |
haftmann |
clarified scopes
|
changeset |
files
|
| Mon, 27 Jan 2025 07:39:49 +0100 |
haftmann |
more correct SML for SML/NJ
|
changeset |
files
|
| Mon, 27 Jan 2025 07:39:48 +0100 |
haftmann |
more explicit real operations
|
changeset |
files
|
| Sun, 26 Jan 2025 13:27:41 +0000 |
paulson |
merged
|
changeset |
files
|
| Sat, 25 Jan 2025 18:40:21 +0000 |
paulson |
Tidied
|
changeset |
files
|
| Sun, 26 Jan 2025 08:39:44 +0100 |
haftmann |
merged
|
changeset |
files
|
| Sat, 25 Jan 2025 21:26:42 +0100 |
haftmann |
modernized and streamlined theory
|
changeset |
files
|
| Sat, 25 Jan 2025 23:16:28 +0100 |
wenzelm |
provide somewhat incomplete naproche-20250125 for testing;
|
changeset |
files
|
| Sat, 25 Jan 2025 22:04:07 +0100 |
wenzelm |
conservative update to stackage lts-22.15 and ghc-9.6.6;
|
changeset |
files
|
| Sat, 25 Jan 2025 21:29:27 +0100 |
wenzelm |
conservative update to stack-2.15.7;
|
changeset |
files
|
| Fri, 24 Jan 2025 21:24:42 +0000 |
paulson |
merged
|
changeset |
files
|
| Fri, 24 Jan 2025 17:53:17 +0000 |
paulson |
merged
|
changeset |
files
|
| Fri, 24 Jan 2025 17:53:06 +0000 |
paulson |
Tidying more old proofs
|
changeset |
files
|
| Fri, 24 Jan 2025 20:05:01 +0100 |
wenzelm |
discontinue old Java 17 LTS;
|
changeset |
files
|
| Fri, 24 Jan 2025 19:54:43 +0100 |
wenzelm |
update versions for release -- one behind current jedit-5.7.0;
|
changeset |
files
|
| Fri, 24 Jan 2025 19:35:55 +0100 |
wenzelm |
more explicit system dependencies;
|
changeset |
files
|
| Fri, 24 Jan 2025 19:25:31 +0100 |
wenzelm |
proper executable from "isabelle ocaml_opam env";
|
changeset |
files
|
| Fri, 24 Jan 2025 14:35:47 +0100 |
wenzelm |
update to postgresql-42.7.5;
|
changeset |
files
|
| Fri, 24 Jan 2025 13:06:29 +0100 |
wenzelm |
update to jdk-21.0.6;
|
changeset |
files
|
| Fri, 24 Jan 2025 11:17:32 +0100 |
wenzelm |
update for release;
|
changeset |
files
|
| Fri, 24 Jan 2025 10:56:59 +0100 |
wenzelm |
misc tuning for release;
|
changeset |
files
|
| Fri, 24 Jan 2025 10:48:28 +0100 |
wenzelm |
more NEWS;
|
changeset |
files
|
| Fri, 24 Jan 2025 10:34:21 +0100 |
wenzelm |
more authors;
|
changeset |
files
|
| Fri, 24 Jan 2025 10:22:17 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Thu, 23 Jan 2025 22:29:38 +0100 |
wenzelm |
tuned names: follow HOL Light;
|
changeset |
files
|
| Thu, 23 Jan 2025 22:20:40 +0100 |
wenzelm |
more antiquotations;
|
changeset |
files
|
| Thu, 23 Jan 2025 22:19:30 +0100 |
wenzelm |
support for @{instantiate (no_beta) ...};
|
changeset |
files
|
| Thu, 23 Jan 2025 20:46:26 +0100 |
wenzelm |
minor performance tuning: more fine-grained guard to skip irrelevant items;
|
changeset |
files
|
| Thu, 23 Jan 2025 20:06:14 +0100 |
wenzelm |
proper treatment of variables with the same name, but different sorts/types: this routinely happens in HOL Light (see also 0e2f019477e2), as well as theory "HOL-Algebra.Algebraic_Closure_Type" (line 77);
|
changeset |
files
|
| Thu, 23 Jan 2025 14:25:31 +0100 |
wenzelm |
tuned output;
|
changeset |
files
|
| Wed, 22 Jan 2025 22:50:39 +0100 |
wenzelm |
minor performance tuning: omit redundant inst_cterm;
|
changeset |
files
|
| Wed, 22 Jan 2025 22:37:38 +0100 |
wenzelm |
tuned signature: more operations;
|
changeset |
files
|
| Wed, 22 Jan 2025 22:22:19 +0100 |
wenzelm |
misc tuning: more concise operations on prems (without change of exceptions);
|
changeset |
files
|
| Wed, 22 Jan 2025 21:35:05 +0100 |
wenzelm |
tuned: prefer Thm.prem_of, which differes wrt. exceptions that are not handled here;
|
changeset |
files
|
| Wed, 22 Jan 2025 21:31:45 +0100 |
wenzelm |
tuned signature: more explicit operations;
|
changeset |
files
|
| Wed, 22 Jan 2025 19:34:04 +0100 |
wenzelm |
tuned: more direct Thm.cprem_of;
|
changeset |
files
|
| Tue, 21 Jan 2025 23:28:34 +0100 |
wenzelm |
misc tuning;
|
changeset |
files
|
| Tue, 21 Jan 2025 23:17:21 +0100 |
wenzelm |
tuned names;
|
changeset |
files
|
| Tue, 21 Jan 2025 23:15:03 +0100 |
wenzelm |
more direct emulation of HOL Light inferences: prefer Pure rules over HOL thms;
|
changeset |
files
|
| Tue, 21 Jan 2025 19:49:13 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 21 Jan 2025 19:26:39 +0100 |
wenzelm |
misc tuning: prefer specific variants of Thm.dest_comb;
|
changeset |
files
|
| Tue, 21 Jan 2025 19:26:09 +0100 |
wenzelm |
more robust: explicit check for "Trueprop";
|
changeset |
files
|
| Tue, 21 Jan 2025 16:59:57 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 21 Jan 2025 16:50:46 +0100 |
wenzelm |
more robust: explicit check for "Trueprop";
|
changeset |
files
|
| Tue, 21 Jan 2025 16:22:15 +0100 |
wenzelm |
clarified signature: more uniform cterm operations, without context;
|
changeset |
files
|
| Tue, 21 Jan 2025 16:12:27 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 21 Jan 2025 16:09:51 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 21 Jan 2025 11:16:48 +0100 |
wenzelm |
misc tuning: more antiquotations;
|
changeset |
files
|
| Tue, 21 Jan 2025 15:48:39 +0100 |
wenzelm |
clarified exceptions;
|
changeset |
files
|
| Tue, 21 Jan 2025 00:01:31 +0100 |
wenzelm |
tuned names, following HOL Light sources;
|
changeset |
files
|
| Mon, 20 Jan 2025 13:03:50 +0100 |
wenzelm |
more robust alignments for HOL Light Release-3.0.0;
|
changeset |
files
|
| Mon, 20 Jan 2025 23:30:06 +0100 |
wenzelm |
provide num_Axiom for HOL Light Release-3.0.0;
|
changeset |
files
|
| Mon, 20 Jan 2025 23:07:04 +0100 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Mon, 20 Jan 2025 23:00:17 +0100 |
wenzelm |
more comments;
|
changeset |
files
|
| Mon, 20 Jan 2025 22:53:51 +0100 |
wenzelm |
cleanup generated bounds;
|
changeset |
files
|
| Mon, 20 Jan 2025 12:11:36 +0100 |
wenzelm |
discontinue special treatment of HOL Light CONJUNCTS: this is better done in Isabelle;
|
changeset |
files
|
| Mon, 20 Jan 2025 11:38:47 +0100 |
wenzelm |
clarified bundle names, in terms of the "offline" tool;
|
changeset |
files
|
| Sun, 19 Jan 2025 23:48:17 +0100 |
wenzelm |
proper result from "offline" tool;
|
changeset |
files
|
| Sun, 19 Jan 2025 21:02:03 +0100 |
wenzelm |
optional maps.lst;
|
changeset |
files
|
| Sun, 19 Jan 2025 15:36:12 +0100 |
wenzelm |
tuned output: proper progress;
|
changeset |
files
|
| Sun, 19 Jan 2025 15:13:42 +0100 |
wenzelm |
support tracing (with proper guard);
|
changeset |
files
|
| Sun, 19 Jan 2025 14:33:14 +0100 |
wenzelm |
more README;
|
changeset |
files
|
| Sun, 19 Jan 2025 14:23:13 +0100 |
wenzelm |
allow to load additional HOL Light files, after "hol.ml";
|
changeset |
files
|
| Sat, 18 Jan 2025 23:46:46 +0100 |
wenzelm |
more complete bundle;
|
changeset |
files
|
| Sat, 18 Jan 2025 23:37:44 +0100 |
wenzelm |
tuned README;
|
changeset |
files
|
| Sat, 18 Jan 2025 23:28:49 +0100 |
wenzelm |
proper settings;
|
changeset |
files
|
| Sat, 18 Jan 2025 23:19:23 +0100 |
wenzelm |
clarified compression;
|
changeset |
files
|
| Sat, 18 Jan 2025 22:41:33 +0100 |
wenzelm |
clarified patches: avoid duplication;
|
changeset |
files
|
| Sat, 18 Jan 2025 22:29:47 +0100 |
wenzelm |
clarified patches;
|
changeset |
files
|
| Sat, 18 Jan 2025 22:25:47 +0100 |
wenzelm |
more explicit stages, with timing messages;
|
changeset |
files
|
| Sat, 18 Jan 2025 21:13:48 +0100 |
wenzelm |
avoid redundant repository clone;
|
changeset |
files
|