| Tue, 14 Jan 2025 22:35:03 +0000 |
paulson |
Some work on an ancient theory file. And a weird failure in Float.thy
default tip
|
changeset |
files
|
| Tue, 14 Jan 2025 21:50:44 +0000 |
paulson |
simplified old proofs
|
changeset |
files
|
| Tue, 14 Jan 2025 18:46:58 +0000 |
paulson |
polished messy proofs
|
changeset |
files
|
| Mon, 13 Jan 2025 21:17:40 +0100 |
nipkow |
moved lemmas to book
|
changeset |
files
|
| Sun, 12 Jan 2025 23:07:50 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Sun, 12 Jan 2025 22:40:56 +0100 |
wenzelm |
tuned messages: more verbosity;
|
changeset |
files
|
| Sun, 12 Jan 2025 22:16:17 +0100 |
wenzelm |
more explicit default_port;
|
changeset |
files
|
| Sun, 12 Jan 2025 22:05:22 +0100 |
wenzelm |
tuned messages;
|
changeset |
files
|
| Sun, 12 Jan 2025 21:45:49 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 12 Jan 2025 21:39:57 +0100 |
wenzelm |
proper initialization of settings: avoid accidental intrusion from parent process environment;
|
changeset |
files
|
| Sun, 12 Jan 2025 21:38:38 +0100 |
wenzelm |
clarified solr_data directory, provided via settings;
|
changeset |
files
|
| Sun, 12 Jan 2025 21:26:30 +0100 |
wenzelm |
explicit settings FIND_FACTS_WEB and option -w, outside of source (immutable) directory;
|
changeset |
files
|
| Sun, 12 Jan 2025 21:10:32 +0100 |
wenzelm |
tuned message;
|
changeset |
files
|
| Sun, 12 Jan 2025 21:07:23 +0100 |
wenzelm |
implicit session build, similar to "isabelle export";
|
changeset |
files
|
| Sun, 12 Jan 2025 16:15:45 +0100 |
wenzelm |
tuned message;
|
changeset |
files
|
| Sun, 12 Jan 2025 16:15:37 +0100 |
wenzelm |
proper Console_Progress as for other command-line tools;
|
changeset |
files
|
| Sun, 12 Jan 2025 16:03:43 +0100 |
wenzelm |
tuned messages: more formal;
|
changeset |
files
|
| Sun, 12 Jan 2025 15:58:30 +0100 |
wenzelm |
clarified signature: progress is usually optional;
|
changeset |
files
|
| Sun, 12 Jan 2025 15:54:32 +0100 |
wenzelm |
clarified names: "peek" usually refers to evolving mutable state;
|
changeset |
files
|
| Sun, 12 Jan 2025 15:53:50 +0100 |
wenzelm |
more to check;
|
changeset |
files
|
| Sun, 12 Jan 2025 15:52:15 +0100 |
wenzelm |
tuned: avoid "open" in ML and "import _" in Scala;
|
changeset |
files
|
| Sun, 12 Jan 2025 14:23:18 +0100 |
wenzelm |
tuned messages;
|
changeset |
files
|
| Sun, 12 Jan 2025 14:21:22 +0100 |
wenzelm |
tuned headers;
|
changeset |
files
|
| Sun, 12 Jan 2025 14:19:06 +0100 |
wenzelm |
more to check;
|
changeset |
files
|
| Sun, 12 Jan 2025 14:16:21 +0100 |
wenzelm |
clarified names;
|
changeset |
files
|
| Sun, 12 Jan 2025 14:14:30 +0100 |
wenzelm |
clarified signature and modules;
|
changeset |
files
|
| Sun, 12 Jan 2025 14:08:02 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 12 Jan 2025 13:54:44 +0100 |
wenzelm |
avoid conflict with slf4j from sqlite (see also dcddfe4f43a3), notably this message on "isabelle find_facts":
|
changeset |
files
|
| Sun, 12 Jan 2025 13:42:01 +0100 |
wenzelm |
misc tuning;
|
changeset |
files
|
| Sun, 12 Jan 2025 13:41:00 +0100 |
wenzelm |
tuned: fewer warnings in IntelliJ IDEA;
|
changeset |
files
|
| Sun, 12 Jan 2025 13:27:47 +0100 |
wenzelm |
tuned headers;
|
changeset |
files
|
| Sun, 12 Jan 2025 13:27:11 +0100 |
wenzelm |
tuned headers;
|
changeset |
files
|
| Sun, 12 Jan 2025 13:09:42 +0100 |
wenzelm |
more NEWS + CONTRIBUTORS;
|
changeset |
files
|
| Sun, 12 Jan 2025 12:54:25 +0100 |
wenzelm |
tuned comments;
|
changeset |
files
|
| Sun, 12 Jan 2025 00:05:01 +0100 |
wenzelm |
tool wrappers with specific java options, notably classpath "$SOLR_JARS";
|
changeset |
files
|
| Sat, 11 Jan 2025 23:33:55 +0100 |
wenzelm |
clarified options;
|
changeset |
files
|
| Sat, 11 Jan 2025 23:24:32 +0100 |
wenzelm |
proper component src/Tools/Find_Facts;
|
changeset |
files
|
| Sat, 11 Jan 2025 23:19:10 +0100 |
wenzelm |
components for find_facts;
|
changeset |
files
|
| Sat, 11 Jan 2025 23:17:08 +0100 |
wenzelm |
suppress duplicate slf4j-api --- already provided by sqlite;
|
changeset |
files
|
| Sat, 11 Jan 2025 22:18:47 +0100 |
wenzelm |
clarified solr settings;
|
changeset |
files
|
| Sat, 11 Jan 2025 21:58:47 +0100 |
wenzelm |
proper platform.exe;
|
changeset |
files
|
| Sat, 11 Jan 2025 21:51:06 +0100 |
wenzelm |
activate admin tools;
|
changeset |
files
|
| Sat, 11 Jan 2025 21:31:13 +0100 |
wenzelm |
original sources of find-facts 271b5af0c4c8;
|
changeset |
files
|
| Sun, 12 Jan 2025 21:16:09 +0000 |
paulson |
Simplified a lot of messy proofs
|
changeset |
files
|
| Fri, 10 Jan 2025 21:08:18 +0100 |
haftmann |
compatibility with Scala 3
|
changeset |
files
|
| Fri, 10 Jan 2025 18:35:46 +0100 |
haftmann |
more correct code generation for string literals
|
changeset |
files
|
| Fri, 10 Jan 2025 17:13:27 +0100 |
nipkow |
made lemma visible
|
changeset |
files
|
| Fri, 10 Jan 2025 15:48:20 +0000 |
paulson |
fixed a typo
|
changeset |
files
|
| Fri, 10 Jan 2025 15:11:56 +0000 |
paulson |
Correction to pretty printing for set intervals, allowing a line break if necessary for a large expression
|
changeset |
files
|
| Thu, 09 Jan 2025 13:18:37 +0100 |
Lukas Bartl |
tuned documentation and order of instantiated facts
|
changeset |
files
|
| Thu, 09 Jan 2025 23:06:17 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Thu, 09 Jan 2025 14:53:05 +0100 |
wenzelm |
update cygwin near 3.5.5-1, see also https://cygwin.com/pipermail/cygwin-announce/2024-December/012023.html
|
changeset |
files
|
| Thu, 09 Jan 2025 08:33:11 +0100 |
haftmann |
direct symbolic implementations of and, or, xor on integer
|
changeset |
files
|
| Thu, 09 Jan 2025 10:13:05 +0100 |
haftmann |
corrected
|
changeset |
files
|
| Wed, 08 Jan 2025 15:49:52 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 08 Jan 2025 14:35:30 +0100 |
wenzelm |
remove special cases for CVC4 that are actually unused (see also 6273d4c8325b and 1f1c5d85d232);
|
changeset |
files
|
| Wed, 08 Jan 2025 14:30:17 +0100 |
wenzelm |
rebuild cvc5 component (still inactive);
|
changeset |
files
|
| Wed, 08 Jan 2025 15:10:09 +0100 |
desharna |
tuned spacing
|
changeset |
files
|
| Wed, 08 Jan 2025 15:00:35 +0100 |
desharna |
merged
|
changeset |
files
|
| Wed, 08 Jan 2025 14:51:32 +0100 |
desharna |
tuned Sledgehammer caching
|
changeset |
files
|
| Mon, 23 Dec 2024 19:38:16 +0100 |
Lukas Bartl |
Rename "suggest_of" to "instantiate"
|
changeset |
files
|
| Wed, 08 Jan 2025 05:38:13 +0100 |
nipkow |
merged
|
changeset |
files
|
| Wed, 08 Jan 2025 05:37:40 +0100 |
nipkow |
added lemmas
|
changeset |
files
|
| Tue, 07 Jan 2025 22:07:46 +0100 |
wenzelm |
discontinue old / inaccurate show_brackets (see also a4f09493d929 and ca9f5dbab880);
|
changeset |
files
|
| Tue, 07 Jan 2025 21:39:38 +0100 |
wenzelm |
more markup, notaly for LaTeX output: treat record fields as quasi-consts;
|
changeset |
files
|
| Tue, 07 Jan 2025 20:47:42 +0100 |
wenzelm |
tuned: more direct string comparison (see also 6e25f82056ad, where the explanation was actually wrong: about fast_string_ord instead of string_ord);
|
changeset |
files
|
| Tue, 07 Jan 2025 20:32:15 +0100 |
wenzelm |
update release name;
|
changeset |
files
|
| Tue, 07 Jan 2025 15:28:11 +0100 |
wenzelm |
Added tag Isabelle2025-RC0 for changeset bcb793b951c0
|
changeset |
files
|
| Mon, 06 Jan 2025 16:38:46 +0100 |
wenzelm |
proper NEWS section;
Isabelle2025-RC0
|
changeset |
files
|
| Mon, 06 Jan 2025 16:35:59 +0100 |
wenzelm |
proper latin "A" instead of greek "Alpha";
|
changeset |
files
|
| Mon, 06 Jan 2025 16:01:52 +0100 |
wenzelm |
update to current jcef-1.0.61;
|
changeset |
files
|
| Mon, 06 Jan 2025 15:33:35 +0100 |
wenzelm |
recovered "isabelle component_jcef" from bf537a75e872, adapted to 9fe5d8c70352 and 2a99fcb283ee;
|
changeset |
files
|
| Sun, 05 Jan 2025 22:28:05 +0100 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Sun, 05 Jan 2025 21:17:36 +0100 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Sun, 05 Jan 2025 18:10:34 +0100 |
wenzelm |
more robust afp_repository, with regular hgweb URLs;
|
changeset |
files
|
| Sun, 05 Jan 2025 16:22:36 +0100 |
wenzelm |
more documentation;
|
changeset |
files
|
| Sun, 05 Jan 2025 15:30:04 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Sun, 05 Jan 2025 15:18:54 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 05 Jan 2025 15:18:30 +0100 |
wenzelm |
tuned (NB: string_ord is required here for its precedence on length);
|
changeset |
files
|
| Sun, 05 Jan 2025 15:04:42 +0100 |
wenzelm |
more robust: ensure that Nginx is not superseded by implicit Apache dependencies (Ubuntu 24.04);
|
changeset |
files
|
| Sun, 05 Jan 2025 13:24:17 +0100 |
wenzelm |
tuned NEWS;
|
changeset |
files
|
| Sun, 05 Jan 2025 13:21:10 +0100 |
wenzelm |
drop obsolete URLs;
|
changeset |
files
|
| Sat, 04 Jan 2025 23:20:05 +0100 |
wenzelm |
updated Ubuntu versions;
|
changeset |
files
|
| Sat, 04 Jan 2025 23:14:10 +0100 |
wenzelm |
more robust defaults, notably for Ubuntu 24.04;
|
changeset |
files
|
| Sat, 04 Jan 2025 20:24:12 +0100 |
haftmann |
delegate computation to integer thoroughly
|
changeset |
files
|
| Sat, 04 Jan 2025 21:38:13 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Sat, 04 Jan 2025 21:33:08 +0100 |
wenzelm |
more robust: ensure that /run/sshd is present, which is required for ExecStartPre phase;
|
changeset |
files
|
| Sat, 04 Jan 2025 20:59:41 +0100 |
wenzelm |
some support for Ubuntu 24.04;
|
changeset |
files
|
| Sat, 04 Jan 2025 16:22:05 +0100 |
wenzelm |
tuned names: more uniform;
|
changeset |
files
|
| Sat, 04 Jan 2025 15:09:47 +0100 |
wenzelm |
update NEWS / documentation / descriptions for Phorge (formerly Phabricator);
|
changeset |
files
|
| Sat, 04 Jan 2025 15:03:23 +0100 |
wenzelm |
unused;
|
changeset |
files
|
| Sat, 04 Jan 2025 12:51:59 +0100 |
wenzelm |
follow Phorge 2024 week 35;
|
changeset |
files
|
| Sat, 04 Jan 2025 17:38:45 +0100 |
haftmann |
separate theory for tests checking bit operations
|
changeset |
files
|
| Sat, 04 Jan 2025 14:41:30 +0100 |
haftmann |
optionally use shift operations on target numerals for efficient execution
|
changeset |
files
|
| Sat, 04 Jan 2025 14:25:56 +0100 |
haftmann |
some bit operations on target numerals
|
changeset |
files
|
| Fri, 03 Jan 2025 22:35:28 +0100 |
wenzelm |
rebuild E 3.1 on Windows/Cygwin, with patch for proper interrupts;
|
changeset |
files
|
| Thu, 02 Jan 2025 16:59:42 +0100 |
wenzelm |
misc tuning and clarification: more explicit types;
|
changeset |
files
|
| Thu, 02 Jan 2025 12:49:39 +0100 |
wenzelm |
misc tuning and updates for release;
|
changeset |
files
|
| Thu, 02 Jan 2025 12:14:51 +0100 |
wenzelm |
tuned NEWS;
|
changeset |
files
|
| Thu, 02 Jan 2025 12:13:18 +0100 |
wenzelm |
provide component cvc5-1.2.0, including arm64-linux;
|
changeset |
files
|
| Thu, 02 Jan 2025 08:37:55 +0100 |
haftmann |
refined syntax for code_reserved
|
changeset |
files
|
| Thu, 02 Jan 2025 08:37:52 +0100 |
haftmann |
explicit error message for non-existing code target
|
changeset |
files
|
| Wed, 01 Jan 2025 22:06:27 +0100 |
wenzelm |
revert changeset 2f98e3c4592c: avoid conflict with low-level \<^latex> markup;
|
changeset |
files
|
| Wed, 01 Jan 2025 19:42:53 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 01 Jan 2025 19:24:00 +0100 |
wenzelm |
more robust LaTeX setup, notably for Ubuntu 24.04;
|
changeset |
files
|
| Wed, 01 Jan 2025 16:42:28 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 01 Jan 2025 16:33:35 +0100 |
wenzelm |
proper treatment of markup within line indentation, notably for Latex.output_ops;
|
changeset |
files
|
| Tue, 31 Dec 2024 21:37:36 +0100 |
wenzelm |
misc tuning and clarification: more explicit types;
|
changeset |
files
|
| Tue, 31 Dec 2024 15:29:29 +0100 |
wenzelm |
more accurate indentation: retain (before: Double) until it is materialized as blanks;
|
changeset |
files
|
| Tue, 31 Dec 2024 15:09:36 +0100 |
wenzelm |
misc tuning: more uniform;
|
changeset |
files
|
| Mon, 30 Dec 2024 21:36:58 +0100 |
wenzelm |
clarified internal data representation, following push/pop model of Scala version;
|
changeset |
files
|
| Mon, 30 Dec 2024 19:49:50 +0100 |
wenzelm |
tuned names;
|
changeset |
files
|
| Mon, 30 Dec 2024 14:39:33 +0100 |
wenzelm |
more accurate formatting of open_block: markup only, without affecting layout (e.g. via force_next);
|
changeset |
files
|
| Sun, 29 Dec 2024 15:58:47 +0100 |
wenzelm |
tuned: more uniform;
|
changeset |
files
|
| Sun, 29 Dec 2024 15:49:11 +0100 |
wenzelm |
proper treatment of XML.Wrapped_Elem as open_block (amending 7cacedbddba7, but this case is presently unused);
|
changeset |
files
|
| Sun, 29 Dec 2024 15:39:01 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 29 Dec 2024 15:34:28 +0100 |
wenzelm |
unused;
|
changeset |
files
|
| Sun, 29 Dec 2024 15:15:06 +0100 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Sun, 29 Dec 2024 15:05:16 +0100 |
wenzelm |
tuned: more uniform;
|
changeset |
files
|
| Sun, 29 Dec 2024 14:57:13 +0100 |
wenzelm |
tuned: more uniform;
|
changeset |
files
|
| Sun, 29 Dec 2024 13:52:27 +0100 |
wenzelm |
clarified data representation: less redundancy;
|
changeset |
files
|
| Sun, 29 Dec 2024 13:16:26 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 29 Dec 2024 00:00:41 +0100 |
wenzelm |
minor performance tuning;
|
changeset |
files
|
| Sat, 28 Dec 2024 23:44:56 +0100 |
wenzelm |
clarified signature: more direct indent_markup;
|
changeset |
files
|
| Sat, 28 Dec 2024 15:43:30 +0100 |
wenzelm |
more LaTeX markup;
|
changeset |
files
|
| Sat, 28 Dec 2024 21:20:33 +0100 |
nipkow |
Backed out changeset 0ca0a47235e5 (produced Code check failed for Haskell?)
|
changeset |
files
|
| Sat, 28 Dec 2024 18:03:41 +0100 |
nipkow |
tuned
|
changeset |
files
|
| Sat, 28 Dec 2024 16:38:57 +0100 |
nipkow |
merged
|
changeset |
files
|
| Wed, 18 Dec 2024 10:50:59 +0100 |
nipkow |
merged
|
changeset |
files
|
| Wed, 11 Dec 2024 13:44:35 +0100 |
nipkow |
merged
|
changeset |
files
|
| Wed, 11 Dec 2024 13:44:16 +0100 |
nipkow |
tuned slow proof
|
changeset |
files
|
| Fri, 27 Dec 2024 19:57:55 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Fri, 27 Dec 2024 19:49:45 +0100 |
wenzelm |
proper bullet symbols for GUI text -- in contrast to Isabelle \<bullet> 0x002219;
|
changeset |
files
|
| Fri, 27 Dec 2024 18:01:34 +0100 |
wenzelm |
tuned: more direct GUI painting via HTML;
|
changeset |
files
|
| Fri, 27 Dec 2024 17:40:02 +0100 |
wenzelm |
tuned generated output: more standard operations;
|
changeset |
files
|
| Fri, 27 Dec 2024 17:35:24 +0100 |
wenzelm |
tuned GUI output: more uniform;
|
changeset |
files
|
| Fri, 27 Dec 2024 17:30:59 +0100 |
wenzelm |
minor performance tuning;
|
changeset |
files
|
| Fri, 27 Dec 2024 17:26:51 +0100 |
wenzelm |
tuned generated output: more standard operations;
|
changeset |
files
|
| Fri, 27 Dec 2024 17:26:01 +0100 |
wenzelm |
clarified signature: more operations;
|
changeset |
files
|
| Fri, 27 Dec 2024 16:54:48 +0100 |
wenzelm |
more accurate treatment of plain text (amending eede0cf38a63);
|
changeset |
files
|
| Fri, 27 Dec 2024 16:14:16 +0100 |
wenzelm |
clarified signature: more operations;
|
changeset |
files
|
| Fri, 27 Dec 2024 15:59:08 +0100 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Fri, 27 Dec 2024 14:31:38 +0100 |
wenzelm |
tuned, following theories_status.scala;
|
changeset |
files
|
| Thu, 26 Dec 2024 16:42:32 +0100 |
wenzelm |
tuned imports;
|
changeset |
files
|
| Thu, 26 Dec 2024 16:33:46 +0100 |
wenzelm |
tuned GUI output;
|
changeset |
files
|
| Thu, 26 Dec 2024 16:16:28 +0100 |
wenzelm |
clarified signature: ensure uniform style;
|
changeset |
files
|
| Thu, 26 Dec 2024 15:43:07 +0100 |
wenzelm |
tuned GUI output;
|
changeset |
files
|
| Thu, 26 Dec 2024 15:38:57 +0100 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Thu, 26 Dec 2024 15:38:21 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 26 Dec 2024 15:24:21 +0100 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Thu, 26 Dec 2024 15:18:19 +0100 |
wenzelm |
drop redundant space in HTML (see also 18a720984855);
|
changeset |
files
|
| Thu, 26 Dec 2024 13:44:10 +0100 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Thu, 26 Dec 2024 13:22:28 +0100 |
wenzelm |
more robust: proper HTML.output;
|
changeset |
files
|
| Thu, 26 Dec 2024 12:46:45 +0100 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Thu, 26 Dec 2024 12:38:25 +0100 |
wenzelm |
tuned: fewer warnings in IntelliJ IDEA;
|
changeset |
files
|
| Thu, 26 Dec 2024 12:08:05 +0100 |
wenzelm |
clarified output;
|
changeset |
files
|
| Thu, 26 Dec 2024 12:03:56 +0100 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Tue, 24 Dec 2024 16:57:28 +0100 |
wenzelm |
more GUI styles;
|
changeset |
files
|
| Tue, 24 Dec 2024 14:59:56 +0100 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Mon, 23 Dec 2024 14:09:43 +0100 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Sun, 22 Dec 2024 14:21:39 +0100 |
wenzelm |
tuned: fewer warnings in IntelliJ IDEA;
|
changeset |
files
|
| Sun, 22 Dec 2024 14:13:21 +0100 |
wenzelm |
tuned: fewer warnings in IntelliJ IDEA;
|
changeset |
files
|
| Sun, 22 Dec 2024 14:11:31 +0100 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Mon, 23 Dec 2024 21:58:26 +0100 |
haftmann |
some bit operations on target numerals
|
changeset |
files
|
| Mon, 23 Dec 2024 21:22:10 +0100 |
haftmann |
explicit tests for target-language bit operations
|
changeset |
files
|
| Sun, 22 Dec 2024 08:46:03 +0100 |
haftmann |
avoid default simp rule which would produce strange recursive unfolding in presence of bit_eq_iff
|
changeset |
files
|
| Sat, 21 Dec 2024 13:27:20 +0100 |
wenzelm |
update to xz-java-1.10 for further testing (see also fe7238c01809);
|
changeset |
files
|
| Thu, 19 Dec 2024 15:13:33 +0100 |
haftmann |
more default simp rules
|
changeset |
files
|
| Thu, 19 Dec 2024 22:19:27 +0100 |
wenzelm |
back to xz-java-1.9, to see if this improves build_manager stability;
|
changeset |
files
|
| Thu, 19 Dec 2024 17:01:54 +0000 |
paulson |
merged
|
changeset |
files
|
| Thu, 19 Dec 2024 17:01:40 +0000 |
paulson |
revered the hiding of the standard nat theorems
|
changeset |
files
|
| Thu, 19 Dec 2024 16:01:06 +0100 |
desharna |
minor performance tuning; directly try to read file instead of first checking its existence
|
changeset |
files
|
| Thu, 19 Dec 2024 08:26:04 +0100 |
desharna |
merged
|
changeset |
files
|
| Thu, 19 Dec 2024 08:18:21 +0100 |
desharna |
minor performance tuning; avoid constructing path if unused and double construction
|
changeset |
files
|
| Wed, 18 Dec 2024 23:36:51 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 18 Dec 2024 21:06:55 +0100 |
wenzelm |
more markup: for diagnostic purposes of ambig_msgs;
|
changeset |
files
|
| Wed, 18 Dec 2024 16:03:07 +0100 |
wenzelm |
more uniform Markup.notation vs. Markup.expression;
|
changeset |
files
|
| Wed, 18 Dec 2024 14:53:31 +0100 |
wenzelm |
tuned output: suppress vacuous nodes from 07ad0b407d38;
|
changeset |
files
|
| Wed, 18 Dec 2024 13:49:55 +0100 |
wenzelm |
clarified LaTeX presentation: more specific keywords;
|
changeset |
files
|
| Wed, 18 Dec 2024 12:49:42 +0100 |
wenzelm |
clarified literal data;
|
changeset |
files
|
| Wed, 18 Dec 2024 16:48:14 +0100 |
desharna |
merged
|
changeset |
files
|
| Wed, 18 Dec 2024 16:33:32 +0100 |
desharna |
tuned ATP caching in Sledgehammer to consider the command line
|
changeset |
files
|
| Wed, 18 Dec 2024 16:32:49 +0100 |
desharna |
tuned function lines_of_atp_problem to have header lines as proper list elements
|
changeset |
files
|
| Wed, 18 Dec 2024 16:20:34 +0100 |
desharna |
tuned tests for existing directories in Sledgehammer
|
changeset |
files
|
| Wed, 18 Dec 2024 11:59:44 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 18 Dec 2024 11:59:38 +0100 |
wenzelm |
tuned GUI: more informative search_title;
|
changeset |
files
|
| Tue, 17 Dec 2024 23:07:13 +0100 |
wenzelm |
clarified induct rules: proper case_names;
|
changeset |
files
|
| Tue, 17 Dec 2024 15:35:46 +0100 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Tue, 17 Dec 2024 14:56:13 +0100 |
wenzelm |
tuned GUI: trim text as in org.gjt.sp.jedit.search.HyperSearchResult;
|
changeset |
files
|
| Tue, 17 Dec 2024 13:38:52 +0100 |
wenzelm |
clarified GUI: more auto_hovering_button instances;
|
changeset |
files
|
| Tue, 17 Dec 2024 13:14:55 +0100 |
wenzelm |
more robust: prefer official BasicSplitPaneUI operations;
|
changeset |
files
|
| Tue, 17 Dec 2024 12:36:37 +0100 |
wenzelm |
clarified split_pane layout: close on first display, open on first search;
|
changeset |
files
|
| Mon, 16 Dec 2024 22:53:31 +0100 |
wenzelm |
more operations, specifically for FlatLaf;
|
changeset |
files
|
| Wed, 18 Dec 2024 11:02:56 +0100 |
desharna |
added documentation for new Sledehammer option "cache_dir"
|
changeset |
files
|
| Wed, 18 Dec 2024 10:43:44 +0100 |
desharna |
updated affiliation in Sledgehammer documentation
|
changeset |
files
|
| Wed, 18 Dec 2024 10:23:25 +0100 |
desharna |
merged
|
changeset |
files
|
| Wed, 18 Dec 2024 10:21:58 +0100 |
desharna |
added option "cache_dir" to Sledgehammer
|
changeset |
files
|
| Mon, 16 Dec 2024 21:08:43 +0100 |
haftmann |
more simp rules on word conversions
|
changeset |
files
|
| Mon, 16 Dec 2024 19:22:54 +0100 |
wenzelm |
spelling;
|
changeset |
files
|
| Mon, 16 Dec 2024 19:09:14 +0100 |
wenzelm |
update to xz-java-1.10;
|
changeset |
files
|
| Mon, 16 Dec 2024 13:55:26 +0100 |
wenzelm |
update to zstd-jni-1.5.6-8;
|
changeset |
files
|
| Mon, 16 Dec 2024 13:51:32 +0100 |
wenzelm |
update to sqlite-3.47.1.0;
|
changeset |
files
|
| Mon, 16 Dec 2024 13:32:36 +0100 |
wenzelm |
updated to postgresql-42.7.4;
|
changeset |
files
|
| Mon, 16 Dec 2024 13:13:05 +0100 |
wenzelm |
update to llncs-2.25;
|
changeset |
files
|
| Mon, 16 Dec 2024 13:08:32 +0100 |
wenzelm |
update to jsoup-1.18.3;
|
changeset |
files
|
| Mon, 16 Dec 2024 12:55:39 +0100 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Sun, 15 Dec 2024 22:58:48 +0100 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Sun, 15 Dec 2024 21:39:43 +0100 |
wenzelm |
avoid duplicate markup, notably from "CONST c";
|
changeset |
files
|
| Sun, 15 Dec 2024 21:15:18 +0100 |
wenzelm |
clarified pretty_entity for syntax consts without mixfix annotation (see also 43c4817375bf and d622145603ee);
|
changeset |
files
|
| Sun, 15 Dec 2024 20:22:29 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 15 Dec 2024 20:12:45 +0100 |
wenzelm |
clarified signature (see also 2157039256d3);
|
changeset |
files
|
| Sun, 15 Dec 2024 14:59:57 +0100 |
wenzelm |
more syntax bundles, e.g. to explore terms without notation;
|
changeset |
files
|
| Sat, 14 Dec 2024 23:48:45 +0100 |
wenzelm |
commands 'syntax_types' and 'syntax_consts' now work in a local theory context;
|
changeset |
files
|
| Sat, 14 Dec 2024 22:26:27 +0100 |
wenzelm |
tuned names;
|
changeset |
files
|
| Sat, 14 Dec 2024 22:04:39 +0100 |
wenzelm |
tuned signature: avoid shadowing;
|
changeset |
files
|
| Sat, 14 Dec 2024 21:47:20 +0100 |
wenzelm |
syntax translations now work in a local theory context;
|
changeset |
files
|
| Sat, 14 Dec 2024 17:35:53 +0100 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Sat, 14 Dec 2024 16:58:53 +0100 |
wenzelm |
clarified signature and modules;
|
changeset |
files
|
| Fri, 13 Dec 2024 23:23:07 +0100 |
wenzelm |
minor performance tuning: avoid excessive Library.insert and Symbol.explode operations;
|
changeset |
files
|
| Thu, 12 Dec 2024 22:53:06 +0100 |
wenzelm |
tuned whitespace;
|
changeset |
files
|
| Thu, 12 Dec 2024 17:07:17 +0100 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Thu, 12 Dec 2024 17:07:09 +0100 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Thu, 12 Dec 2024 16:57:06 +0100 |
wenzelm |
clarified class/locale reasoning: avoid side-stepping constraints;
|
changeset |
files
|
| Thu, 12 Dec 2024 15:45:29 +0100 |
wenzelm |
clarified default_sort: "cpo" for bootstrap, "domain" for main HOLCF;
|
changeset |
files
|
| Thu, 12 Dec 2024 12:35:59 +0100 |
wenzelm |
clarified specification context;
|
changeset |
files
|
| Wed, 11 Dec 2024 12:04:27 +0100 |
wenzelm |
activate e-3.1 as proposed by Martin Desharnais;
|
changeset |
files
|
| Wed, 11 Dec 2024 12:03:01 +0100 |
wenzelm |
more robust: avoid spurious crash of text_area.getText() in Active_Area.update();
|
changeset |
files
|
| Wed, 11 Dec 2024 11:18:52 +0100 |
wenzelm |
proper bundle binomial_syntax;
|
changeset |
files
|
| Wed, 11 Dec 2024 11:14:50 +0100 |
wenzelm |
build component for cvc5-1.2.0;
|
changeset |
files
|
| Wed, 11 Dec 2024 10:40:57 +0100 |
wenzelm |
tuned whitespace;
|
changeset |
files
|
| Wed, 11 Dec 2024 10:28:12 +0100 |
wenzelm |
clarified default_sort;
|
changeset |
files
|
| Tue, 10 Dec 2024 22:59:13 +0100 |
wenzelm |
fewer theories;
|
changeset |
files
|
| Tue, 10 Dec 2024 22:40:07 +0100 |
wenzelm |
fewer theories;
|
changeset |
files
|
| Tue, 10 Dec 2024 21:43:04 +0100 |
wenzelm |
fewer theories (in contrast to 05ca920cd94b);
|
changeset |
files
|
| Tue, 10 Dec 2024 21:06:04 +0100 |
wenzelm |
more accurate markup for "CONST c";
|
changeset |
files
|
| Tue, 10 Dec 2024 19:47:47 +0100 |
wenzelm |
tuned markup;
|
changeset |
files
|
| Tue, 10 Dec 2024 19:23:55 +0100 |
wenzelm |
proper LaTeX setup (amending 41b387d47739);
|
changeset |
files
|
| Tue, 10 Dec 2024 16:37:09 +0100 |
wenzelm |
more LaTeX markup for printed entities;
|
changeset |
files
|
| Tue, 10 Dec 2024 14:42:56 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 10 Dec 2024 10:52:46 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 08 Dec 2024 20:13:40 +0100 |
wenzelm |
more HTML markup (without rendering);
|
changeset |
files
|
| Sun, 08 Dec 2024 20:09:14 +0100 |
wenzelm |
more markup (without rendering): class, type constructor, term constant --- similar to free, bound, etc.;
|
changeset |
files
|
| Sun, 08 Dec 2024 19:05:05 +0100 |
wenzelm |
tuned: more robust wrt. changes the Markup space;
|
changeset |
files
|
| Sun, 08 Dec 2024 15:12:20 +0100 |
wenzelm |
tuned: prefer explicit names of inferred types;
|
changeset |
files
|
| Sun, 08 Dec 2024 14:27:06 +0100 |
wenzelm |
more accurate HTML markup: suppress text_color that has_syntax (amending b57996a0688c);
|
changeset |
files
|
| Sun, 08 Dec 2024 11:49:55 +0100 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Sun, 08 Dec 2024 00:05:35 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 07 Dec 2024 23:40:29 +0100 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Sat, 07 Dec 2024 23:50:18 +0100 |
wenzelm |
clarified term positions and markup: syntax = true means this is via concrete syntax;
|
changeset |
files
|
| Sat, 07 Dec 2024 23:08:51 +0100 |
wenzelm |
tuned signature: more operations;
|
changeset |
files
|
| Sat, 07 Dec 2024 21:49:05 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 07 Dec 2024 21:42:59 +0100 |
wenzelm |
clarified signature: more explicit operations;
|
changeset |
files
|
| Sat, 07 Dec 2024 16:07:48 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 07 Dec 2024 16:03:05 +0100 |
wenzelm |
tuned whitespace;
|
changeset |
files
|
| Sat, 07 Dec 2024 15:00:43 +0100 |
wenzelm |
clarified signature and caching;
|
changeset |
files
|
| Sat, 07 Dec 2024 11:59:51 +0100 |
wenzelm |
clarified GUI: prefer user documents, which are typically without chapter;
|
changeset |
files
|
| Sat, 07 Dec 2024 11:13:02 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 06 Dec 2024 23:07:09 +0100 |
wenzelm |
obsolete;
|
changeset |
files
|
| Fri, 06 Dec 2024 22:40:43 +0100 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Fri, 06 Dec 2024 21:27:07 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Fri, 06 Dec 2024 20:46:24 +0100 |
wenzelm |
NEWS;
|
changeset |
files
|
| Fri, 06 Dec 2024 20:26:33 +0100 |
wenzelm |
clarified renaming of bounds, using Syntax_Trans.variant_bounds: avoid structures and fixed variables with syntax;
|
changeset |
files
|
| Fri, 06 Dec 2024 15:20:43 +0100 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Fri, 06 Dec 2024 13:33:25 +0100 |
wenzelm |
clarified printing of consts: rename apart from all bounds, and thus avoid old Term.declare_free_names with its adhoc policy ("as they are printed");
|
changeset |
files
|
| Tue, 03 Dec 2024 22:46:24 +0100 |
wenzelm |
prefer Term.variant_bounds: bounds vs. frees, no attempt at consts;
|
changeset |
files
|
| Mon, 02 Dec 2024 22:16:29 +0100 |
wenzelm |
more elementary operation Term.variant_bounds: only for bounds vs. frees, no consts, no tfrees;
|
changeset |
files
|
| Mon, 02 Dec 2024 20:35:12 +0100 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Mon, 02 Dec 2024 18:53:45 +0100 |
wenzelm |
clarified modules;
|
changeset |
files
|
| Mon, 02 Dec 2024 14:30:10 +0100 |
wenzelm |
more accurate extern_const: avoid clash with frees;
|
changeset |
files
|
| Mon, 02 Dec 2024 14:08:28 +0100 |
wenzelm |
more direct Proof_Context.lookup_free -- bypass redundancy of Proof_Context.check_const;
|
changeset |
files
|
| Mon, 02 Dec 2024 11:45:42 +0100 |
wenzelm |
clarified signature: uniform context;
|
changeset |
files
|
| Mon, 02 Dec 2024 11:36:53 +0100 |
wenzelm |
clarified signature: uniform context;
|
changeset |
files
|
| Mon, 02 Dec 2024 11:22:44 +0100 |
wenzelm |
proper context for extern operation: observe local options;
|
changeset |
files
|
| Mon, 02 Dec 2024 11:08:36 +0100 |
wenzelm |
proper context for extern/check operation: observe local options like names_unique;
|
changeset |
files
|
| Sun, 01 Dec 2024 22:14:13 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 01 Dec 2024 21:46:54 +0100 |
wenzelm |
tuned signature: more operations;
|
changeset |
files
|
| Thu, 05 Dec 2024 19:44:53 +0100 |
nipkow |
added Halting problem theory
|
changeset |
files
|
| Thu, 05 Dec 2024 15:49:48 +0100 |
desharna |
merged
|
changeset |
files
|
| Fri, 29 Sep 2023 15:27:43 +0200 |
desharna |
added parallel_group_size option to Mirabelle
|
changeset |
files
|
| Thu, 05 Dec 2024 15:23:46 +0100 |
desharna |
adapted bash files to use cartouches
|
changeset |
files
|
| Mon, 02 Dec 2024 12:38:27 +0100 |
nipkow |
tuned
|
changeset |
files
|
| Sun, 01 Dec 2024 21:14:56 +0100 |
wenzelm |
clarified names context: proper context, without consts;
|
changeset |
files
|
| Sun, 01 Dec 2024 21:13:57 +0100 |
wenzelm |
clarified names context: proper context, without consts;
|
changeset |
files
|
| Sun, 01 Dec 2024 18:12:24 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 01 Dec 2024 14:24:10 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 01 Dec 2024 14:01:47 +0100 |
wenzelm |
clarified signature: more operations;
|
changeset |
files
|
| Sat, 30 Nov 2024 23:30:36 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Sat, 30 Nov 2024 22:33:21 +0100 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Sat, 30 Nov 2024 22:02:36 +0100 |
wenzelm |
tuned names/scopes;
|
changeset |
files
|
| Sat, 30 Nov 2024 21:01:59 +0100 |
wenzelm |
tuned signature: more operations;
|
changeset |
files
|
| Sat, 30 Nov 2024 19:21:38 +0100 |
wenzelm |
eliminate historic clone (see also 550e36c6a2d1);
|
changeset |
files
|
| Sat, 30 Nov 2024 17:14:30 +0100 |
wenzelm |
tuned signature: more operations;
|
changeset |
files
|
| Sat, 30 Nov 2024 16:42:22 +0100 |
wenzelm |
clarified 'unbundle' polarity, according to algebraic group laws;
|
changeset |
files
|
| Sat, 30 Nov 2024 16:01:58 +0100 |
wenzelm |
tuned signature: more operations;
|
changeset |
files
|
| Sat, 30 Nov 2024 13:41:38 +0100 |
wenzelm |
tuned: more direct use of Name.context operations;
|
changeset |
files
|
| Sat, 30 Nov 2024 13:40:57 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 30 Nov 2024 13:27:15 +0100 |
wenzelm |
misc tuning and clarification: more direct use of Name.context operations;
|
changeset |
files
|
| Sat, 30 Nov 2024 13:31:43 +0100 |
wenzelm |
tuned signature: more operations;
|
changeset |
files
|
| Sat, 30 Nov 2024 12:30:18 +0100 |
wenzelm |
tuned: more direct use of Name.context operations;
|
changeset |
files
|
| Fri, 29 Nov 2024 17:40:15 +0100 |
wenzelm |
clarified signature: shorten common cases;
|
changeset |
files
|
| Fri, 29 Nov 2024 11:26:17 +0100 |
wenzelm |
tuned: more standard Name.build_context, although that is a bit longer;
|
changeset |
files
|
| Fri, 29 Nov 2024 00:25:03 +0100 |
wenzelm |
clarified signature: more uniform;
|
changeset |
files
|
| Thu, 28 Nov 2024 19:35:30 +0100 |
wenzelm |
omit redundant combinators (amending 7456a64bc4f6);
|
changeset |
files
|
| Thu, 28 Nov 2024 14:12:13 +0100 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Fri, 29 Nov 2024 10:35:47 +0100 |
blanchet |
fixed bugs found by Stepan Holub
|
changeset |
files
|
| Wed, 27 Nov 2024 16:52:04 +0100 |
nipkow |
merged
|
changeset |
files
|
| Wed, 27 Nov 2024 16:51:50 +0100 |
nipkow |
added lemmas
|
changeset |
files
|
| Fri, 22 Nov 2024 20:21:36 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Thu, 21 Nov 2024 23:07:06 +0100 |
wenzelm |
more ambitious Search_Result.gui_text, using Swing HTML3 (NB: TreeCellRenderer cannot do this, because it is not updated for each entry);
|
changeset |
files
|
| Thu, 21 Nov 2024 12:47:42 +0100 |
wenzelm |
clarified signature and object initialization;
|
changeset |
files
|
| Tue, 19 Nov 2024 22:55:09 +0100 |
wenzelm |
clarified default: avoid copies;
|
changeset |
files
|
| Tue, 19 Nov 2024 22:48:18 +0100 |
wenzelm |
suppress odd icons for documents and folders;
|
changeset |
files
|
| Tue, 19 Nov 2024 22:41:57 +0100 |
wenzelm |
support for modified tree cell renderer;
|
changeset |
files
|
| Tue, 19 Nov 2024 15:46:22 +0100 |
wenzelm |
clarified signature: avoid implicit functionality;
|
changeset |
files
|
| Tue, 19 Nov 2024 15:35:03 +0100 |
wenzelm |
re-use Output_Area;
|
changeset |
files
|
| Tue, 19 Nov 2024 15:34:58 +0100 |
wenzelm |
re-use Output_Area;
|
changeset |
files
|
| Tue, 19 Nov 2024 15:25:11 +0100 |
wenzelm |
re-use Output_Area;
|
changeset |
files
|
| Tue, 19 Nov 2024 10:52:02 +0100 |
wenzelm |
re-use Output_Area with search results;
|
changeset |
files
|
| Tue, 19 Nov 2024 10:40:19 +0100 |
wenzelm |
re-use Output_Area with search results;
|
changeset |
files
|
| Tue, 19 Nov 2024 10:14:22 +0100 |
wenzelm |
more thorough init;
|
changeset |
files
|
| Tue, 19 Nov 2024 10:11:37 +0100 |
wenzelm |
clarified signature: prefer defaults for Output_Dockable (and its variants);
|
changeset |
files
|
| Tue, 19 Nov 2024 10:11:17 +0100 |
wenzelm |
unused;
|
changeset |
files
|
| Mon, 18 Nov 2024 16:48:11 +0100 |
wenzelm |
tuned output: formatting is pointless for proportional font;
|
changeset |
files
|
| Mon, 18 Nov 2024 15:05:31 +0100 |
wenzelm |
clarified Tree_View.init_model: more uniform;
|
changeset |
files
|
| Mon, 18 Nov 2024 14:47:17 +0100 |
wenzelm |
more robust update;
|
changeset |
files
|
| Mon, 18 Nov 2024 14:35:48 +0100 |
wenzelm |
handle tree selection;
|
changeset |
files
|
| Mon, 18 Nov 2024 12:36:56 +0100 |
wenzelm |
Output_Dockable: show search results as tree view;
|
changeset |
files
|
| Mon, 18 Nov 2024 11:12:51 +0100 |
wenzelm |
clarified modules;
|
changeset |
files
|
| Mon, 18 Nov 2024 11:06:53 +0100 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Sun, 17 Nov 2024 20:14:57 +0100 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Sun, 17 Nov 2024 19:59:10 +0100 |
wenzelm |
clarified signature and modules: without GUI change yet;
|
changeset |
files
|
| Sun, 17 Nov 2024 19:49:25 +0100 |
wenzelm |
more operations, to support search within output panel;
|
changeset |
files
|
| Sun, 17 Nov 2024 13:57:50 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 22 Nov 2024 16:05:42 +0000 |
paulson |
Introduced the function some_elem for grabbing an element from a non-empty set, and simplified the theorem the_elem_image_unique
|
changeset |
files
|
| Fri, 22 Nov 2024 14:54:00 +0000 |
paulson |
Patch by Stepan Holub, plus tweaks
|
changeset |
files
|
| Fri, 22 Nov 2024 13:23:27 +0000 |
paulson |
patch to vector_matrix_mult by Alexander Pach
|
changeset |
files
|
| Tue, 19 Nov 2024 18:47:12 +0100 |
Fabian Huch |
try0: cleaned up output;
|
changeset |
files
|
| Mon, 18 Nov 2024 13:30:02 +0100 |
Fabian Huch |
try0: insert extra facts into state instead of goal, since some methods (e.g. metis) won't work otherwise;
|
changeset |
files
|
| Mon, 18 Nov 2024 12:35:44 +0100 |
Fabian Huch |
avoid informatik.tu-muenchen.de domain: soon to be discontinued;
|
changeset |
files
|
| Sun, 17 Nov 2024 21:20:26 +0100 |
nipkow |
renamed Discrete -> Discrete_Functions to avoid name clashes;
|
changeset |
files
|
| Sun, 17 Nov 2024 09:50:54 +0100 |
nipkow |
Use Var to maintain the difference between function and locale parameters
|
changeset |
files
|
| Sat, 16 Nov 2024 22:46:33 +0100 |
nipkow |
tuned
|
changeset |
files
|
| Sat, 16 Nov 2024 21:36:34 +0100 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Sat, 16 Nov 2024 20:22:26 +0100 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Sat, 16 Nov 2024 19:54:30 +0100 |
wenzelm |
minor performance tuning: avoided repeated metric initialization;
|
changeset |
files
|
| Sat, 16 Nov 2024 19:07:24 +0100 |
wenzelm |
tuned signature: more operations;
|
changeset |
files
|
| Sat, 16 Nov 2024 15:04:41 +0100 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Fri, 15 Nov 2024 23:25:18 +0100 |
wenzelm |
more NEWS;
|
changeset |
files
|
| Fri, 15 Nov 2024 23:20:24 +0100 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Fri, 15 Nov 2024 21:43:22 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Fri, 15 Nov 2024 21:04:51 +0100 |
wenzelm |
enforce rebuild of Isabelle/ML and Isabelle/Scala;
|
changeset |
files
|
| Fri, 15 Nov 2024 20:48:41 +0100 |
wenzelm |
update to jedit-20241115 (see also ecd62f7b3644 and d92d754b5dd9);
|
changeset |
files
|
| Fri, 15 Nov 2024 20:44:49 +0100 |
wenzelm |
more patches for the sake of SideKick 1.8 vs. jEdit 5.7.0: provide missing GUIUtilities.isPopupTrigger, avoid StatusBar messages (which often don't fit);
|
changeset |
files
|
| Fri, 15 Nov 2024 16:50:44 +0100 |
wenzelm |
tuned comments;
|
changeset |
files
|
| Fri, 15 Nov 2024 16:08:56 +0100 |
wenzelm |
clarified key events: cancel output selection, before input selection;
|
changeset |
files
|
| Fri, 15 Nov 2024 16:04:26 +0100 |
wenzelm |
proper focus to support subsequent copy-paste via keyboard;
|
changeset |
files
|
| Fri, 15 Nov 2024 16:01:41 +0100 |
wenzelm |
more accurate initial FontRenderContext, notably on macOS, Windows, or Linux with "env GDK_SCALE=2";
|
changeset |
files
|
| Fri, 15 Nov 2024 15:18:48 +0100 |
wenzelm |
removed obsolete option: jEdit 5.7.0 can be built with default jdk;
|
changeset |
files
|
| Fri, 15 Nov 2024 13:31:36 +0100 |
wenzelm |
more rebust mechanics of refresh (see also 82110cbcf9a1 and 2d9b6e32632d): painter.getFontRenderContext might be in undefined state (notably on macOS due to display scaling);
|
changeset |
files
|
| Fri, 15 Nov 2024 13:08:48 +0100 |
wenzelm |
less ambitious selection;
|
changeset |
files
|
| Fri, 15 Nov 2024 21:37:26 +0100 |
nipkow |
mv Discrete to Discrete_Cpo to avoid theory name clashes
|
changeset |
files
|
| Thu, 14 Nov 2024 11:33:51 +0100 |
wenzelm |
disable 2d9b6e32632d for now: unknown problems on macOS;
|
changeset |
files
|
| Thu, 14 Nov 2024 11:12:11 +0100 |
wenzelm |
clarified mouse selection, avoid conflict of double-click with single-click (follow hyperlink);
|
changeset |
files
|
| Thu, 14 Nov 2024 10:50:49 +0100 |
wenzelm |
more careful isConsumed() / consume() for key and mouse events;
|
changeset |
files
|
| Wed, 13 Nov 2024 23:11:06 +0100 |
nipkow |
merged
|
changeset |
files
|
| Wed, 13 Nov 2024 23:10:58 +0100 |
nipkow |
added field input_eqns to record the list of equations (the specification)
|
changeset |
files
|
| Wed, 13 Nov 2024 20:14:24 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 13 Nov 2024 20:14:17 +0100 |
wenzelm |
more NEWS;
|
changeset |
files
|
| Wed, 13 Nov 2024 20:10:34 +0100 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Wed, 13 Nov 2024 15:14:48 +0100 |
wenzelm |
more ambitious mouse handler: double-click selects highlight_area;
|
changeset |
files
|
| Wed, 13 Nov 2024 14:54:08 +0100 |
wenzelm |
more accurate mouse handler: only for single clicks, consume accepted event;
|
changeset |
files
|
| Wed, 13 Nov 2024 11:53:02 +0100 |
wenzelm |
more ambitious scrolling: retain original scroll position if possible;
|
changeset |
files
|
| Wed, 13 Nov 2024 10:56:17 +0100 |
wenzelm |
more ambitious scrolling: retain bottom position after output;
|
changeset |
files
|
| Tue, 12 Nov 2024 22:30:45 +0100 |
wenzelm |
performance tuning: cache for Rich_Text.format, notably for incremental tracing;
|
changeset |
files
|
| Tue, 12 Nov 2024 11:32:07 +0100 |
wenzelm |
clarified persistent values: Command.Results does not suitable for caching, because it contains all other messages;
|
changeset |
files
|
| Tue, 12 Nov 2024 11:16:36 +0100 |
wenzelm |
omit redundant compact_source (see e1abca2527da): Command_Span.unparsed consists of one token with the original source;
|
changeset |
files
|
| Tue, 12 Nov 2024 11:04:54 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 11 Nov 2024 13:15:55 +0100 |
wenzelm |
minor performance tuning: avoid duplication of Symbol.spaces (e.g. from Pretty.formatted);
|
changeset |
files
|
| Mon, 11 Nov 2024 12:47:51 +0100 |
wenzelm |
clarified signature and modules;
|
changeset |
files
|
| Mon, 11 Nov 2024 12:19:45 +0100 |
wenzelm |
performance tuning for macOS (after update of "jedit" component): old OpenGL works better for text rendering;
|
changeset |
files
|
| Sun, 10 Nov 2024 16:04:56 +0100 |
wenzelm |
performance tuning: more incremental update of buffer content;
|
changeset |
files
|
| Sun, 10 Nov 2024 15:11:04 +0100 |
wenzelm |
obsolete;
|
changeset |
files
|
| Sun, 10 Nov 2024 15:10:51 +0100 |
wenzelm |
clarified: more uniform results;
|
changeset |
files
|
| Sun, 10 Nov 2024 14:58:05 +0100 |
wenzelm |
clarified signature: inline org.gjt.sp.jedit.textarea.TextArea.setText();
|
changeset |
files
|
| Sun, 10 Nov 2024 13:40:28 +0100 |
wenzelm |
minor performance tuning: avoid concatenation of existing string material;
|
changeset |
files
|
| Sun, 10 Nov 2024 12:56:38 +0100 |
wenzelm |
clarified signature and data storage: incremental lazy values;
|
changeset |
files
|
| Sun, 10 Nov 2024 12:33:20 +0100 |
wenzelm |
tuned comments;
|
changeset |
files
|
| Sun, 10 Nov 2024 12:29:32 +0100 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Sun, 10 Nov 2024 12:23:41 +0100 |
wenzelm |
clarified modules;
|
changeset |
files
|
| Sun, 10 Nov 2024 12:15:31 +0100 |
wenzelm |
clarified margin operations (again, reverting 4794576828df);
|
changeset |
files
|
| Sun, 10 Nov 2024 11:55:36 +0100 |
wenzelm |
clarified modules;
|
changeset |
files
|
| Sun, 10 Nov 2024 11:38:23 +0100 |
wenzelm |
more reactive interrupts (via Future.cancel);
|
changeset |
files
|
| Sat, 09 Nov 2024 21:34:38 +0100 |
wenzelm |
Document.Snapshot: support for multiple snippet_commands;
|
changeset |
files
|
| Sat, 09 Nov 2024 16:39:33 +0100 |
wenzelm |
more robust: make double-sure that this is the correct output, not a different version from concurrent GUI_Thread.later;
|
changeset |
files
|
| Sat, 09 Nov 2024 16:34:14 +0100 |
wenzelm |
clarified signature: include standard margin in object equality;
|
changeset |
files
|
| Sat, 09 Nov 2024 16:01:07 +0100 |
wenzelm |
performance tuning: prefer asynchronous Pretty.formatted, which actually takes longer than Command.rich_text (see also 97964515a676, where Pretty.formatted was on the GUI thread, maybe for the sake of java.awt.FontMetrics at that time);
|
changeset |
files
|
| Wed, 13 Nov 2024 15:00:17 +0000 |
paulson |
The ceillog2 function (thanks to Manuel Eberl), replacing two copies of Ceil_Log2
|
changeset |
files
|
| Fri, 08 Nov 2024 22:52:29 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Fri, 08 Nov 2024 19:18:32 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Fri, 08 Nov 2024 18:39:35 +0100 |
wenzelm |
clarified signature: avoid pointless alias (see also c82a1620b274 and 22aeec526ffd);
|
changeset |
files
|
| Fri, 08 Nov 2024 18:34:33 +0100 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Fri, 08 Nov 2024 16:57:48 +0100 |
wenzelm |
tuned GUI: avoid wasting space with proportional fonts;
|
changeset |
files
|
| Fri, 08 Nov 2024 16:52:06 +0100 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Fri, 08 Nov 2024 15:08:36 +0100 |
wenzelm |
more accurate pretty_margin for proportional fonts;
|
changeset |
files
|
| Fri, 08 Nov 2024 14:44:29 +0100 |
wenzelm |
clarified signature: more uniform;
|
changeset |
files
|
| Fri, 08 Nov 2024 13:55:54 +0100 |
wenzelm |
tuned: fewer warnings in IntelliJ IDEA;
|
changeset |
files
|
| Fri, 08 Nov 2024 13:42:25 +0100 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Fri, 08 Nov 2024 13:37:13 +0100 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Fri, 08 Nov 2024 13:27:26 +0100 |
wenzelm |
clarified signature with subtle change of semantics: output consists of individual messages that are formatted (and separated) internally;
|
changeset |
files
|
| Thu, 07 Nov 2024 20:43:25 +0100 |
wenzelm |
more accurate message boundaries;
|
changeset |
files
|
| Thu, 07 Nov 2024 20:37:11 +0100 |
wenzelm |
tuned whitespace;
|
changeset |
files
|
| Thu, 07 Nov 2024 20:29:52 +0100 |
wenzelm |
clarified signature: more robust type XML.Elem;
|
changeset |
files
|
| Thu, 07 Nov 2024 20:08:50 +0100 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Thu, 07 Nov 2024 20:02:10 +0100 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Thu, 07 Nov 2024 16:13:58 +0100 |
wenzelm |
clarified output representation: postpone Pretty.separate;
|
changeset |
files
|
| Thu, 07 Nov 2024 16:03:53 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 07 Nov 2024 15:42:35 +0100 |
wenzelm |
tuned: fewer warnings in IntelliJ IDEA;
|
changeset |
files
|
| Thu, 07 Nov 2024 13:30:40 +0100 |
wenzelm |
clarified signature: more accurate types;
|
changeset |
files
|
| Thu, 07 Nov 2024 13:26:31 +0100 |
wenzelm |
tuned signature: more standard names;
|
changeset |
files
|
| Thu, 07 Nov 2024 13:22:59 +0100 |
wenzelm |
more uniform pretty_text_area.zoom via its zoom_component;
|
changeset |
files
|
| Thu, 07 Nov 2024 12:35:55 +0100 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Thu, 07 Nov 2024 12:32:44 +0100 |
wenzelm |
tuned signature: more standard names;
|
changeset |
files
|
| Thu, 07 Nov 2024 12:26:36 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 07 Nov 2024 12:17:18 +0100 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Thu, 07 Nov 2024 12:08:32 +0100 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Thu, 07 Nov 2024 11:46:21 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 07 Nov 2024 11:35:39 +0100 |
wenzelm |
revert 1206400b9b48: proper Node.unapply for Node.apply(null);
|
changeset |
files
|
| Wed, 06 Nov 2024 22:04:05 +0100 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Wed, 06 Nov 2024 16:07:30 +0100 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Wed, 06 Nov 2024 15:52:31 +0100 |
wenzelm |
clarified signature, with subtle change of semantics: proper non-null result;
|
changeset |
files
|
| Wed, 06 Nov 2024 15:38:45 +0100 |
wenzelm |
clarified modules;
|
changeset |
files
|
| Wed, 06 Nov 2024 15:17:39 +0100 |
wenzelm |
more robust and uniform metric, still with special treatment motivated by jEdit (see also 0cdfce0bf956);
|
changeset |
files
|
| Wed, 06 Nov 2024 11:05:18 +0100 |
wenzelm |
misc tuning;
|
changeset |
files
|
| Fri, 08 Nov 2024 18:13:55 +0100 |
Fabian Huch |
try0: avoid mapping background theory -- should be handled by Context_Position visibility;
|
changeset |
files
|
| Thu, 31 Oct 2024 11:35:24 +0100 |
Fabian Huch |
try0: stop early if more subgoals are created;
|
changeset |
files
|
| Fri, 25 Oct 2024 16:38:15 +0200 |
Fabian Huch |
try0: filter out untagged thms;
|
changeset |
files
|
| Thu, 24 Oct 2024 19:13:49 +0200 |
Fabian Huch |
try0: support literal facts;
|
changeset |
files
|
| Thu, 24 Oct 2024 16:46:25 +0200 |
Fabian Huch |
try0: add 'use' modifier for thms to insert;
|
changeset |
files
|
| Thu, 24 Oct 2024 16:45:09 +0200 |
Fabian Huch |
try0: use extra thms via insert;
|
changeset |
files
|
| Thu, 24 Oct 2024 18:25:17 +0200 |
Fabian Huch |
clarified: proper type for facts;
|
changeset |
files
|
| Thu, 24 Oct 2024 18:16:36 +0200 |
Fabian Huch |
clarified: proper type;
|
changeset |
files
|
| Thu, 24 Oct 2024 14:08:28 +0200 |
Fabian Huch |
tuned;
|
changeset |
files
|
| Thu, 24 Oct 2024 14:07:13 +0200 |
Fabian Huch |
tuned;
|
changeset |
files
|
| Thu, 24 Oct 2024 11:37:41 +0200 |
Fabian Huch |
try0: pass tagged thms for better control;
|
changeset |
files
|
| Tue, 22 Oct 2024 17:31:54 +0200 |
Fabian Huch |
clarified: proper return type;
|
changeset |
files
|
| Tue, 22 Oct 2024 14:34:13 +0200 |
Fabian Huch |
improve try0: solve multiple subgoals at once, if possible;
|
changeset |
files
|
| Tue, 22 Oct 2024 14:31:25 +0200 |
Fabian Huch |
tuned: unused parameter;
|
changeset |
files
|
| Fri, 08 Nov 2024 11:18:08 +0100 |
nipkow |
tuned
|
changeset |
files
|
| Thu, 07 Nov 2024 16:21:57 +0100 |
nipkow |
better termination behaviour
|
changeset |
files
|
| Wed, 06 Nov 2024 18:10:39 +0100 |
nipkow |
uniform name T_f for closed-form lemmas for function T_f
|
changeset |
files
|
| Wed, 06 Nov 2024 16:27:06 +0100 |
nipkow |
More time for primitive functions
|
changeset |
files
|
| Wed, 06 Nov 2024 16:19:45 +0100 |
nipkow |
merged Reverse into Time_Funs
|
changeset |
files
|
| Tue, 05 Nov 2024 23:51:44 +0100 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Tue, 05 Nov 2024 23:45:39 +0100 |
wenzelm |
tuned description: plain text documentation is also supported;
|
changeset |
files
|
| Tue, 05 Nov 2024 23:27:47 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Tue, 05 Nov 2024 23:01:09 +0100 |
wenzelm |
update to jdk-21.0.5;
|
changeset |
files
|
| Tue, 05 Nov 2024 22:05:50 +0100 |
wenzelm |
misc tuning and clarification: Doc.Entry supports both plain files and pdf documents;
|
changeset |
files
|
| Tue, 05 Nov 2024 19:59:30 +0100 |
nipkow |
tuned proofs
|
changeset |
files
|
| Tue, 05 Nov 2024 19:52:15 +0100 |
nipkow |
added missing definitions
|
changeset |
files
|
| Mon, 04 Nov 2024 22:36:42 +0100 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Mon, 04 Nov 2024 22:05:20 +0100 |
wenzelm |
clarified modules;
|
changeset |
files
|
| Mon, 04 Nov 2024 21:54:34 +0100 |
wenzelm |
support value-oriented Font_Metric, e.g. for caching Pretty output;
|
changeset |
files
|
| Mon, 04 Nov 2024 21:25:26 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 04 Nov 2024 21:05:11 +0100 |
wenzelm |
unused;
|
changeset |
files
|
| Mon, 04 Nov 2024 21:05:05 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 04 Nov 2024 21:00:31 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 04 Nov 2024 20:55:01 +0100 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Mon, 04 Nov 2024 14:50:21 +0100 |
wenzelm |
more accurate Symbol.Metric, following 6eccae338770;
|
changeset |
files
|
| Mon, 04 Nov 2024 14:39:27 +0100 |
wenzelm |
tuned rendering, notably for HiDPI on Linux (see also ca7e2c21b104);
|
changeset |
files
|
| Mon, 04 Nov 2024 14:10:21 +0100 |
wenzelm |
proper parentheses, for the sake of IntelliJ IDEA;
|
changeset |
files
|
| Mon, 04 Nov 2024 12:58:05 +0100 |
wenzelm |
clarified modules;
|
changeset |
files
|
| Mon, 04 Nov 2024 12:22:24 +0100 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Mon, 04 Nov 2024 11:21:19 +0100 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Mon, 04 Nov 2024 11:21:04 +0100 |
wenzelm |
tuned GUI (again, see 0521e65af41e);
|
changeset |
files
|
| Sun, 03 Nov 2024 22:29:07 +0100 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Sun, 03 Nov 2024 21:12:50 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 03 Nov 2024 21:04:12 +0100 |
wenzelm |
tuned comments;
|
changeset |
files
|
| Sun, 03 Nov 2024 20:53:12 +0100 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Sun, 03 Nov 2024 20:23:19 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 03 Nov 2024 20:15:12 +0100 |
wenzelm |
tuned names;
|
changeset |
files
|
| Sun, 03 Nov 2024 20:05:06 +0100 |
wenzelm |
more robust;
|
changeset |
files
|
| Sun, 03 Nov 2024 20:01:26 +0100 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Sun, 03 Nov 2024 20:00:54 +0100 |
wenzelm |
unused;
|
changeset |
files
|
| Sun, 03 Nov 2024 19:38:30 +0100 |
wenzelm |
clarified signature: more explicit types;
|
changeset |
files
|
| Sun, 03 Nov 2024 14:11:01 +0100 |
wenzelm |
tuned GUI;
|
changeset |
files
|
| Sat, 02 Nov 2024 20:27:41 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 02 Nov 2024 20:24:53 +0100 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Sat, 02 Nov 2024 20:14:44 +0100 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Sat, 02 Nov 2024 16:22:06 +0100 |
wenzelm |
tuned imports;
|
changeset |
files
|
| Sat, 02 Nov 2024 16:11:02 +0100 |
wenzelm |
tuned: remove redundant checks;
|
changeset |
files
|
| Sat, 02 Nov 2024 16:08:26 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 02 Nov 2024 16:03:26 +0100 |
wenzelm |
clarified modules;
|
changeset |
files
|
| Sat, 02 Nov 2024 15:59:58 +0100 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Sat, 02 Nov 2024 15:42:37 +0100 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Sat, 02 Nov 2024 15:35:43 +0100 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Sat, 02 Nov 2024 15:28:17 +0100 |
wenzelm |
tuned: fewer warnings in IntelliJ IDEA;
|
changeset |
files
|
| Sat, 02 Nov 2024 15:22:50 +0100 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Sat, 02 Nov 2024 14:58:50 +0100 |
wenzelm |
clarified modules: more re-usable;
|
changeset |
files
|
| Sat, 02 Nov 2024 14:56:13 +0100 |
wenzelm |
proper protocol messages (amending 7a1f9e571046);
|
changeset |
files
|
| Fri, 01 Nov 2024 19:20:52 +0100 |
wenzelm |
clarified treatment of caret_range: better support for multiple (unrelated) selections;
|
changeset |
files
|
| Fri, 01 Nov 2024 19:11:40 +0100 |
wenzelm |
tuned whitespace;
|
changeset |
files
|
| Fri, 01 Nov 2024 18:55:47 +0100 |
wenzelm |
support incremental isabelle.select-structure --- like select-block, but based on selection instead of caret;
|
changeset |
files
|
| Fri, 01 Nov 2024 18:17:03 +0100 |
wenzelm |
clarified rendering: entity acts as atomic notation / expression;
|
changeset |
files
|
| Fri, 01 Nov 2024 18:12:40 +0100 |
wenzelm |
more rendering for Markup.COMMAND_SPAN, following Rendering.structure_elements;
|
changeset |
files
|
| Fri, 01 Nov 2024 17:13:42 +0100 |
wenzelm |
more NEWS;
|
changeset |
files
|
| Fri, 01 Nov 2024 16:57:33 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Fri, 01 Nov 2024 16:53:10 +0100 |
wenzelm |
support Isabelle/jEdit action isabelle.select_structure;
|
changeset |
files
|
| Fri, 01 Nov 2024 15:40:31 +0100 |
wenzelm |
more operations;
|
changeset |
files
|
| Tue, 29 Oct 2024 21:51:21 +0100 |
wenzelm |
clarified text;
|
changeset |
files
|
| Tue, 29 Oct 2024 12:30:15 +0100 |
wenzelm |
update to jedit5.7.0;
|
changeset |
files
|
| Mon, 28 Oct 2024 09:43:28 +0100 |
wenzelm |
GUI option "editor_auto_hovering" for Output panel;
|
changeset |
files
|
| Mon, 28 Oct 2024 09:40:28 +0100 |
wenzelm |
update to scala-3.3.4 LTS;
|
changeset |
files
|
| Mon, 28 Oct 2024 08:48:31 +0100 |
wenzelm |
removed obsolete markup for "open_block" (see also d5ad89fda714): Isabelle/Scala directly supports XML.Elem pretty-printing;
|
changeset |
files
|
| Fri, 01 Nov 2024 14:10:52 +0000 |
paulson |
Library material from Eberl's Parallel_Shear_Sort
|
changeset |
files
|
| Fri, 01 Nov 2024 12:15:53 +0000 |
paulson |
Trying to clean up these horribly ugly old proofs, but the requirement of constructivity makes it very difficult
|
changeset |
files
|
| Thu, 31 Oct 2024 18:43:32 +0100 |
Manuel Eberl |
use automatically generated time function in HOL-Data_Structures.Selection
|
changeset |
files
|
| Thu, 31 Oct 2024 15:46:53 +0100 |
nipkow |
merged
|
changeset |
files
|
| Thu, 31 Oct 2024 15:46:33 +0100 |
nipkow |
better time_functions (let)
|
changeset |
files
|
| Thu, 31 Oct 2024 14:58:53 +0100 |
Fabian Huch |
less hidden configuration;
|
changeset |
files
|
| Thu, 31 Oct 2024 14:56:59 +0100 |
Fabian Huch |
proper passwordless smtp check: must be null;
|
changeset |
files
|
| Thu, 31 Oct 2024 09:24:10 +0100 |
blanchet |
adjusted documentation
|
changeset |
files
|
| Tue, 29 Oct 2024 10:26:06 +0100 |
nipkow |
more attribute tuning
|
changeset |
files
|
| Tue, 29 Oct 2024 07:41:52 +0100 |
nipkow |
tuned attributes
|
changeset |
files
|
| Mon, 28 Oct 2024 18:48:28 +0100 |
nipkow |
merged
|
changeset |
files
|
| Mon, 28 Oct 2024 18:48:14 +0100 |
nipkow |
added lemmas
|
changeset |
files
|
| Sun, 27 Oct 2024 22:35:02 +0100 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Sun, 27 Oct 2024 20:11:08 +0100 |
wenzelm |
tuned NEWS;
|
changeset |
files
|
| Sun, 27 Oct 2024 19:57:29 +0100 |
wenzelm |
markup for "..." notation;
|
changeset |
files
|
| Sun, 27 Oct 2024 15:30:00 +0100 |
wenzelm |
more robust: avoid non-authentic translations;
|
changeset |
files
|
| Sun, 27 Oct 2024 12:54:58 +0100 |
wenzelm |
tuned whitespace of sources;
|
changeset |
files
|
| Sun, 27 Oct 2024 12:47:27 +0100 |
wenzelm |
update documentation;
|
changeset |
files
|
| Sun, 27 Oct 2024 12:32:40 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 27 Oct 2024 12:23:48 +0100 |
wenzelm |
update documentation: print mode "latex" only affects syntax tables, but output of symbols;
|
changeset |
files
|
| Sun, 27 Oct 2024 12:13:34 +0100 |
wenzelm |
misc tuning and clarification;
|
changeset |
files
|
| Sun, 27 Oct 2024 11:48:32 +0100 |
wenzelm |
clarified section structure;
|
changeset |
files
|
| Sun, 27 Oct 2024 11:46:04 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 27 Oct 2024 11:34:51 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 27 Oct 2024 11:31:42 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 27 Oct 2024 11:22:34 +0100 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Sun, 27 Oct 2024 11:13:42 +0100 |
wenzelm |
clarified symbolic output: avoid redundant "block" element for open_block = true;
|
changeset |
files
|
| Sun, 27 Oct 2024 11:02:21 +0100 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Sat, 26 Oct 2024 20:18:51 +0200 |
wenzelm |
clarified (again): Markup.intensify is already part of Variable.markup_fixed for undeclared variable, Markup.fixed is already part of Mariable.markup;
|
changeset |
files
|
| Sat, 26 Oct 2024 16:07:31 +0200 |
wenzelm |
more accurate Symbol.length;
|
changeset |
files
|
| Sat, 26 Oct 2024 16:07:03 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 25 Oct 2024 22:22:21 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Fri, 25 Oct 2024 16:03:58 +0200 |
wenzelm |
more inner-syntax markup;
|
changeset |
files
|
| Fri, 25 Oct 2024 15:48:40 +0200 |
wenzelm |
obsolete (see a8502d492dde);
|
changeset |
files
|
| Fri, 25 Oct 2024 15:39:27 +0200 |
wenzelm |
minor performance tuning;
|
changeset |
files
|
| Fri, 25 Oct 2024 13:43:12 +0200 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Fri, 25 Oct 2024 11:31:16 +0200 |
wenzelm |
more inner-syntax markup;
|
changeset |
files
|
| Fri, 25 Oct 2024 17:01:23 +0200 |
nipkow |
merged
|
changeset |
files
|
| Fri, 25 Oct 2024 16:57:17 +0200 |
nipkow |
time_fun: lambdas and lets work now
|
changeset |
files
|
| Fri, 25 Oct 2024 15:31:58 +0200 |
blanchet |
variable instantiation in Sledgehammer and Metis
|
changeset |
files
|
| Thu, 24 Oct 2024 22:05:57 +0200 |
wenzelm |
prefer rewrite_term_yoyo for improved performance and occasionally better results (conforming to Ast.normalize);
|
changeset |
files
|
| Thu, 24 Oct 2024 12:44:48 +0200 |
wenzelm |
revert b35c2aa05fcf: redundant due to 89ea66c2045b, if object-logic judgment lacks delimiters;
|
changeset |
files
|
| Thu, 24 Oct 2024 12:42:41 +0200 |
wenzelm |
clarified position constraints: omit redundant information, e.g. for implicit object-logic judgment;
|
changeset |
files
|
| Thu, 24 Oct 2024 11:50:20 +0200 |
wenzelm |
unused (see 0199acc01aa8);
|
changeset |
files
|
| Thu, 24 Oct 2024 00:26:14 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 24 Oct 2024 00:20:21 +0200 |
wenzelm |
more robust: avoid ambiguity of contract_abbrevs;
|
changeset |
files
|
| Wed, 23 Oct 2024 23:46:07 +0200 |
wenzelm |
misc tuning: more concise (or hermetic) pointfree style;
|
changeset |
files
|
| Wed, 23 Oct 2024 21:57:46 +0200 |
wenzelm |
provide rewrite_term_yoyo, which is analogous to Ast.normalize;
|
changeset |
files
|
| Wed, 23 Oct 2024 15:09:02 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Wed, 23 Oct 2024 14:59:06 +0200 |
wenzelm |
tuned names;
|
changeset |
files
|
| Wed, 23 Oct 2024 14:05:31 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 23 Oct 2024 13:58:29 +0200 |
wenzelm |
misc tuning and clarification;
|
changeset |
files
|
| Wed, 23 Oct 2024 13:30:11 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 23 Oct 2024 13:03:49 +0200 |
wenzelm |
misc tuning and clarification;
|
changeset |
files
|
| Tue, 22 Oct 2024 23:56:48 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Tue, 22 Oct 2024 22:52:27 +0200 |
wenzelm |
adhoc option to disable const constraints, notably for AFP/Isabelle_DOF;
|
changeset |
files
|
| Tue, 22 Oct 2024 22:34:33 +0200 |
wenzelm |
unused;
|
changeset |
files
|
| Tue, 22 Oct 2024 21:29:44 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Tue, 22 Oct 2024 20:53:54 +0200 |
wenzelm |
proper treatment of position constraints;
|
changeset |
files
|
| Tue, 22 Oct 2024 20:05:23 +0200 |
wenzelm |
more liberal ast matching, notably for case-translations in HOLCF that operate on logical consts rather than syntax consts;
|
changeset |
files
|
| Tue, 22 Oct 2024 19:46:05 +0200 |
wenzelm |
more parser markup, based on position constraints for logical mixfix syntax;
|
changeset |
files
|
| Tue, 22 Oct 2024 19:26:40 +0200 |
wenzelm |
more concise representation of term positions;
|
changeset |
files
|
| Tue, 22 Oct 2024 13:39:24 +0200 |
wenzelm |
more robust;
|
changeset |
files
|
| Tue, 22 Oct 2024 12:52:25 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Tue, 22 Oct 2024 12:45:38 +0200 |
wenzelm |
tuned comments;
|
changeset |
files
|
| Tue, 22 Oct 2024 12:41:20 +0200 |
wenzelm |
misc tuning and clarification;
|
changeset |
files
|
| Tue, 22 Oct 2024 12:28:32 +0200 |
wenzelm |
clarified concrete vs. abstract syntax: avoid translations on logical consts;
|
changeset |
files
|
| Tue, 22 Oct 2024 12:15:02 +0200 |
wenzelm |
misc tuning and clarification;
|
changeset |
files
|
| Tue, 22 Oct 2024 12:03:46 +0200 |
wenzelm |
clarified markers for syntax consts: avoid overlap with logical consts;
|
changeset |
files
|
| Tue, 22 Oct 2024 17:32:34 +0200 |
Fabian Huch |
update ci mail address;
|
changeset |
files
|
| Mon, 21 Oct 2024 22:58:14 +0200 |
wenzelm |
minor performance tuning;
|
changeset |
files
|
| Mon, 21 Oct 2024 22:28:07 +0200 |
wenzelm |
notable performance tuning (amending a59d9b81be24 and 8976c5bc9e97): avoid costly could_beta_eta_contract, which traverses the whole term;
|
changeset |
files
|
| Mon, 21 Oct 2024 20:02:27 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 21 Oct 2024 14:50:59 +0200 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Mon, 21 Oct 2024 14:33:59 +0200 |
wenzelm |
tuned whitespace;
|
changeset |
files
|
| Mon, 21 Oct 2024 11:55:51 +0200 |
wenzelm |
support multiple positions (non-empty list);
|
changeset |
files
|
| Sun, 20 Oct 2024 22:40:18 +0200 |
wenzelm |
more robust syntax translation;
|
changeset |
files
|
| Sun, 20 Oct 2024 22:39:36 +0200 |
wenzelm |
clarified concrete vs. abstract syntax;
|
changeset |
files
|
| Sun, 20 Oct 2024 21:51:47 +0200 |
wenzelm |
more inner-syntax markup;
|
changeset |
files
|
| Sun, 20 Oct 2024 21:48:38 +0200 |
wenzelm |
clarified concrete vs. abstract syntax;
|
changeset |
files
|
| Sun, 20 Oct 2024 20:32:53 +0200 |
wenzelm |
clarified concrete vs. abstract syntax;
|
changeset |
files
|
| Sun, 20 Oct 2024 18:47:42 +0200 |
wenzelm |
more operations;
|
changeset |
files
|
| Sun, 20 Oct 2024 15:48:06 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 20 Oct 2024 15:37:19 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Sun, 20 Oct 2024 13:41:56 +0200 |
wenzelm |
more operations;
|
changeset |
files
|
| Sun, 20 Oct 2024 13:27:17 +0200 |
wenzelm |
more accurate treatment of constraints: restrict permissive mode to output;
|
changeset |
files
|
| Sun, 20 Oct 2024 13:13:17 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 19 Oct 2024 22:57:43 +0200 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Sat, 19 Oct 2024 22:38:51 +0200 |
wenzelm |
clarified order of tooltips: make it less dependent on report order from ML (which differs for input vs. output);
|
changeset |
files
|
| Sat, 19 Oct 2024 22:20:05 +0200 |
wenzelm |
clarified signature (see also 1de8a8b1ae79);
|
changeset |
files
|
| Sat, 19 Oct 2024 22:01:36 +0200 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Sat, 19 Oct 2024 19:00:19 +0200 |
wenzelm |
more type information;
|
changeset |
files
|
| Sat, 19 Oct 2024 17:16:16 +0200 |
wenzelm |
more type information;
|
changeset |
files
|
| Sat, 19 Oct 2024 17:00:14 +0200 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Sat, 19 Oct 2024 16:54:34 +0200 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Sat, 19 Oct 2024 16:45:05 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Sat, 19 Oct 2024 16:27:00 +0200 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Fri, 18 Oct 2024 21:20:21 +0200 |
wenzelm |
suppress dummyT, e.g. from Type_Annotation.print;
|
changeset |
files
|
| Fri, 18 Oct 2024 21:19:06 +0200 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Fri, 18 Oct 2024 20:48:01 +0200 |
wenzelm |
print type constraints for consts with mixfix syntax;
|
changeset |
files
|
| Fri, 18 Oct 2024 19:00:51 +0200 |
wenzelm |
tuned comments;
|
changeset |
files
|
| Fri, 18 Oct 2024 19:00:13 +0200 |
wenzelm |
obsolete (see 137ea3d464be);
|
changeset |
files
|
| Fri, 18 Oct 2024 16:43:02 +0200 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Fri, 18 Oct 2024 16:42:53 +0200 |
wenzelm |
tuned whitespace;
|
changeset |
files
|
| Fri, 18 Oct 2024 16:37:39 +0200 |
wenzelm |
more inner-syntax markup;
|
changeset |
files
|
| Fri, 18 Oct 2024 16:31:35 +0200 |
wenzelm |
less instrusive rendering for input buffer (in contrast to 264f043c5da1);
|
changeset |
files
|
| Fri, 18 Oct 2024 15:45:38 +0200 |
wenzelm |
clarified inner-syntax markup;
|
changeset |
files
|
| Fri, 18 Oct 2024 15:42:31 +0200 |
wenzelm |
tuned whitespace;
|
changeset |
files
|
| Fri, 18 Oct 2024 15:36:42 +0200 |
wenzelm |
tuned whitespace;
|
changeset |
files
|
| Fri, 18 Oct 2024 14:37:09 +0200 |
wenzelm |
clarified syntax declarations: keep things together;
|
changeset |
files
|
| Fri, 18 Oct 2024 14:35:13 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 18 Oct 2024 14:20:09 +0200 |
wenzelm |
more inner-syntax markup;
|
changeset |
files
|
| Fri, 18 Oct 2024 11:44:05 +0200 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Fri, 18 Oct 2024 11:32:10 +0200 |
wenzelm |
more ambitious rendering: highlight active area for mouse hovering without modifier;
|
changeset |
files
|
| Wed, 16 Oct 2024 23:13:02 +0200 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Wed, 16 Oct 2024 22:07:04 +0200 |
wenzelm |
show_consts_markup is enabled by default;
|
changeset |
files
|
| Wed, 16 Oct 2024 21:41:05 +0200 |
wenzelm |
clarified signature (again, reverting ec1023a5c54c);
|
changeset |
files
|
| Wed, 16 Oct 2024 21:22:37 +0200 |
wenzelm |
clarified signature: more explicit Syntax.print_mode_tabs, depending on print_mode_value ();
|
changeset |
files
|
| Wed, 16 Oct 2024 20:22:20 +0200 |
wenzelm |
redundant;
|
changeset |
files
|
| Wed, 16 Oct 2024 19:44:02 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Wed, 16 Oct 2024 16:20:35 +0200 |
wenzelm |
performance tuning: cache markup and extern operations;
|
changeset |
files
|
| Tue, 15 Oct 2024 23:44:42 +0200 |
wenzelm |
minor performance tuning;
|
changeset |
files
|
| Tue, 15 Oct 2024 16:11:37 +0200 |
wenzelm |
minor performance tuning;
|
changeset |
files
|
| Tue, 15 Oct 2024 14:57:23 +0200 |
wenzelm |
backout somewhat pointless 5ea48342e0ae: no need to declare syntax consts for translations (e.g. constraints);
|
changeset |
files
|
| Tue, 15 Oct 2024 14:55:45 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 15 Oct 2024 14:39:54 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 15 Oct 2024 14:36:37 +0200 |
wenzelm |
revert redundant guard (T = dummyT) from 0278f6d87bad;
|
changeset |
files
|
| Tue, 15 Oct 2024 14:19:58 +0200 |
wenzelm |
allow type constraints for const_syntax;
|
changeset |
files
|
| Tue, 15 Oct 2024 12:18:02 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 14 Oct 2024 19:48:59 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 14 Oct 2024 11:16:11 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 14 Oct 2024 11:13:26 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 14 Oct 2024 11:06:03 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 12 Oct 2024 22:11:38 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Sat, 12 Oct 2024 22:05:37 +0200 |
wenzelm |
misc tuning and clarification;
|
changeset |
files
|
| Sat, 12 Oct 2024 21:21:50 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 12 Oct 2024 19:21:47 +0200 |
wenzelm |
tuned: more readable names;
|
changeset |
files
|
| Sat, 12 Oct 2024 15:00:56 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 12 Oct 2024 14:55:46 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 12 Oct 2024 14:48:10 +0200 |
wenzelm |
misc tuning and clarification;
|
changeset |
files
|
| Sat, 12 Oct 2024 14:29:39 +0200 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Sat, 12 Oct 2024 14:22:19 +0200 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Sat, 12 Oct 2024 14:16:15 +0200 |
wenzelm |
misc tuning and clarification;
|
changeset |
files
|
| Fri, 11 Oct 2024 15:17:37 +0200 |
wenzelm |
eliminate clones: just one Collect_binder_tr';
|
changeset |
files
|
| Fri, 11 Oct 2024 14:15:10 +0200 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Fri, 11 Oct 2024 10:29:47 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 12 Oct 2024 12:45:29 +0900 |
nipkow |
new HO time functions
|
changeset |
files
|
| Thu, 10 Oct 2024 14:13:18 +0200 |
wenzelm |
tuned NEWS;
|
changeset |
files
|
| Thu, 10 Oct 2024 12:20:24 +0200 |
wenzelm |
clarified inner-syntax markup;
|
changeset |
files
|
| Thu, 10 Oct 2024 12:19:50 +0200 |
wenzelm |
more syntax bundles;
|
changeset |
files
|
| Wed, 09 Oct 2024 23:59:49 +0200 |
wenzelm |
more NEWS;
|
changeset |
files
|
| Wed, 09 Oct 2024 23:38:29 +0200 |
wenzelm |
more inner-syntax markup;
|
changeset |
files
|
| Wed, 09 Oct 2024 22:01:33 +0200 |
wenzelm |
back to specific nonterminals (amending 52ed95fa4656): otherwise AFP/CakeML won't terminate;
|
changeset |
files
|
| Wed, 09 Oct 2024 22:00:12 +0200 |
wenzelm |
uniform \<Sum> and \<Prod> syntax, following d10fafeb93c0;
|
changeset |
files
|
| Wed, 09 Oct 2024 14:12:56 +0200 |
wenzelm |
more NEWS;
|
changeset |
files
|
| Wed, 09 Oct 2024 14:08:13 +0200 |
wenzelm |
more accurate datatype_record_syntax;
|
changeset |
files
|
| Wed, 09 Oct 2024 13:25:19 +0200 |
wenzelm |
more syntax bundles, less clones;
|
changeset |
files
|
| Wed, 09 Oct 2024 13:06:55 +0200 |
wenzelm |
more syntax bundles;
|
changeset |
files
|
| Tue, 08 Oct 2024 23:31:06 +0200 |
wenzelm |
more syntax bundles;
|
changeset |
files
|
| Tue, 08 Oct 2024 22:56:27 +0200 |
wenzelm |
more syntax bundles;
|
changeset |
files
|
| Tue, 08 Oct 2024 17:26:31 +0200 |
wenzelm |
clarified bundles for list syntax;
|
changeset |
files
|
| Tue, 08 Oct 2024 16:15:31 +0200 |
wenzelm |
more robust declarations via "no syntax" bundles;
|
changeset |
files
|
| Tue, 08 Oct 2024 16:14:36 +0200 |
wenzelm |
more accurate no_syntax declarations, following ec121999a9cb;
|
changeset |
files
|
| Tue, 08 Oct 2024 16:13:02 +0200 |
wenzelm |
more robust syntax;
|
changeset |
files
|
| Tue, 08 Oct 2024 15:44:52 +0200 |
wenzelm |
avoid syntax clashes;
|
changeset |
files
|
| Tue, 08 Oct 2024 15:44:11 +0200 |
wenzelm |
tuned whitespace, to simplify hypersearch;
|
changeset |
files
|
| Tue, 08 Oct 2024 15:02:17 +0200 |
wenzelm |
avoid syntax clashes;
|
changeset |
files
|
| Tue, 08 Oct 2024 13:13:53 +0200 |
wenzelm |
clarified mixfix annotations;
|
changeset |
files
|
| Tue, 08 Oct 2024 12:10:35 +0200 |
wenzelm |
more inner-syntax markup;
|
changeset |
files
|
| Sun, 06 Oct 2024 22:56:07 +0200 |
wenzelm |
more inner-syntax markup, without pretty blocks;
|
changeset |
files
|
| Sun, 06 Oct 2024 21:55:31 +0200 |
wenzelm |
tuned output;
|
changeset |
files
|
| Sun, 06 Oct 2024 21:54:53 +0200 |
wenzelm |
tuned comments: all times are < 1ms;
|
changeset |
files
|
| Sun, 06 Oct 2024 18:34:35 +0200 |
wenzelm |
support for pretty blocks that are "open" and thus have no impact on formatting, only on markup;
|
changeset |
files
|
| Sun, 06 Oct 2024 13:02:33 +0200 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Sat, 05 Oct 2024 22:46:21 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 05 Oct 2024 22:24:24 +0200 |
wenzelm |
more inner-syntax markup;
|
changeset |
files
|
| Sat, 05 Oct 2024 15:18:49 +0200 |
wenzelm |
ML antiquotation for formally-checked bundle names;
|
changeset |
files
|
| Sat, 05 Oct 2024 14:58:36 +0200 |
wenzelm |
first-class support for "unbundle no foobar_syntax" -- avoid redundant "bundle no_foobar_syntax" definitions;
|
changeset |
files
|
| Fri, 04 Oct 2024 23:38:04 +0200 |
wenzelm |
misc tuning;
|
changeset |
files
|
| Fri, 04 Oct 2024 15:21:01 +0200 |
wenzelm |
documentation for pretty block "notation" markup;
|
changeset |
files
|
| Fri, 04 Oct 2024 13:29:33 +0200 |
wenzelm |
clarified syntax for opening bundles;
|
changeset |
files
|
| Fri, 04 Oct 2024 13:22:35 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 04 Oct 2024 00:26:28 +0200 |
wenzelm |
clarified bundles for syntax modifications;
|
changeset |
files
|
| Fri, 04 Oct 2024 00:00:50 +0200 |
wenzelm |
bundles for syntax modifications seen in AFP;
|
changeset |
files
|
| Thu, 03 Oct 2024 23:34:55 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 03 Oct 2024 13:01:31 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 02 Oct 2024 23:47:07 +0200 |
wenzelm |
more standard bundle names;
|
changeset |
files
|
| Wed, 02 Oct 2024 22:08:52 +0200 |
wenzelm |
provide 'open_bundle' command;
|
changeset |
files
|
| Wed, 02 Oct 2024 20:49:44 +0200 |
wenzelm |
tuned module structure;
|
changeset |
files
|
| Wed, 02 Oct 2024 19:55:07 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 02 Oct 2024 15:36:48 +0200 |
wenzelm |
more inner syntax markup;
|
changeset |
files
|
| Wed, 02 Oct 2024 14:23:28 +0200 |
wenzelm |
more syntax: avoid duplication in AFP;
|
changeset |
files
|
| Wed, 02 Oct 2024 13:34:03 +0200 |
wenzelm |
clarified abbreviation;
|
changeset |
files
|
| Wed, 02 Oct 2024 11:27:19 +0200 |
wenzelm |
tuned whitespace;
|
changeset |
files
|
| Wed, 02 Oct 2024 11:17:47 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 02 Oct 2024 11:08:45 +0200 |
wenzelm |
more NEWS;
|
changeset |
files
|
| Wed, 02 Oct 2024 10:35:44 +0200 |
wenzelm |
more inner syntax markup: HOL-Analysis;
|
changeset |
files
|
| Wed, 02 Oct 2024 10:34:41 +0200 |
wenzelm |
tuned markup;
|
changeset |
files
|
| Tue, 01 Oct 2024 23:36:10 +0200 |
wenzelm |
more inner syntax markup: HOLCF;
|
changeset |
files
|
| Tue, 01 Oct 2024 22:12:11 +0200 |
wenzelm |
more 'no_syntax' bundles;
|
changeset |
files
|
| Tue, 01 Oct 2024 21:35:31 +0200 |
wenzelm |
more robust 'no_syntax' via bundles;
|
changeset |
files
|
| Tue, 01 Oct 2024 21:30:59 +0200 |
wenzelm |
tuned markup;
|
changeset |
files
|
| Tue, 01 Oct 2024 20:39:16 +0200 |
wenzelm |
drop somewhat pointless 'syntax_consts' declarations;
|
changeset |
files
|
| Mon, 30 Sep 2024 23:32:26 +0200 |
wenzelm |
clarified syntax: use outer block (with indent);
|
changeset |
files
|
| Mon, 30 Sep 2024 22:57:45 +0200 |
wenzelm |
clarified syntax: prefer nonterminal "args", use outer block (with indent);
|
changeset |
files
|
| Wed, 02 Oct 2024 18:32:36 +0200 |
Fabian Huch |
proper command kinds;
|
changeset |
files
|
| Wed, 02 Oct 2024 13:51:45 +0200 |
Fabian Huch |
updated vscode_extension;
|
changeset |
files
|
| Wed, 02 Oct 2024 13:50:01 +0200 |
Fabian Huch |
NEWS and CONTRIBUTORS;
|
changeset |
files
|
| Wed, 02 Oct 2024 10:51:11 +0200 |
Fabian Huch |
clarified: add operation;
|
changeset |
files
|
| Wed, 02 Oct 2024 10:39:32 +0200 |
Fabian Huch |
minor tuning;
|
changeset |
files
|
| Fri, 19 Jul 2024 17:08:20 +0200 |
Thomas Lindae |
lsp: added additional commit characters to immediate completions;
|
changeset |
files
|
| Thu, 18 Jul 2024 23:02:49 +0200 |
Thomas Lindae |
vscode: further adjusted default settings and wordPattern for consistent completion popups;
|
changeset |
files
|
| Thu, 18 Jul 2024 17:59:50 +0200 |
Thomas Lindae |
lsp: added more triggerCharacters to make completion popups more consistent;
|
changeset |
files
|
| Thu, 18 Jul 2024 01:18:43 +0200 |
Thomas Lindae |
vscode: added default setting to make completions pop up by themselves;
|
changeset |
files
|
| Thu, 18 Jul 2024 22:08:46 +0200 |
Thomas Lindae |
lsp: improved completions;
|
changeset |
files
|
| Wed, 17 Jul 2024 21:03:56 +0200 |
Thomas Lindae |
vscode: removed unused code;
|
changeset |
files
|
| Wed, 17 Jul 2024 21:02:30 +0200 |
Thomas Lindae |
vscode: removed README because its content is outdated;
|
changeset |
files
|
| Wed, 17 Jul 2024 20:56:27 +0200 |
Thomas Lindae |
vscode: disabled whitespace rendering by default because the whitespace symbol is not monospace;
|
changeset |
files
|
| Tue, 09 Jul 2024 16:47:48 +0200 |
Thomas Lindae |
lsp: added symbol conversion request;
|
changeset |
files
|
| Fri, 05 Jul 2024 21:40:39 +0200 |
Thomas Lindae |
vscode: changed how options are inserted into package.json so that one can still call `npm install` without errors;
|
changeset |
files
|
| Fri, 05 Jul 2024 13:30:07 +0200 |
Thomas Lindae |
vscode: removed unused import;
|
changeset |
files
|
| Fri, 05 Jul 2024 13:16:47 +0200 |
Thomas Lindae |
vscode: changed vscode_unicode_symbols_edits option default to true;
|
changeset |
files
|
| Fri, 05 Jul 2024 13:15:50 +0200 |
Thomas Lindae |
vscode: made uri equality check on actual strings, not on the functions;
|
changeset |
files
|
| Fri, 05 Jul 2024 13:15:05 +0200 |
Thomas Lindae |
vscode: switched document_decoration map to use strings as keys instead of Uris, because Uri equality check is inconsistent;
|
changeset |
files
|
| Mon, 01 Jul 2024 04:34:04 +0200 |
Thomas Lindae |
lsp: added rudimentary indenting to code actions;
|
changeset |
files
|
| Mon, 01 Jul 2024 18:53:27 +0200 |
Thomas Lindae |
vscode: adjusted setting description;
|
changeset |
files
|
| Sun, 30 Jun 2024 15:23:00 +0200 |
Thomas Lindae |
lsp: added support for code actions to apply active sendback markups;
|
changeset |
files
|
| Sun, 30 Jun 2024 15:22:50 +0200 |
Thomas Lindae |
lsp: clarified WorkspaceEdit;
|
changeset |
files
|
| Sun, 30 Jun 2024 15:22:36 +0200 |
Thomas Lindae |
lsp: made TextDocumentEdit accept optional versions;
|
changeset |
files
|
| Sun, 30 Jun 2024 15:32:51 +0200 |
Thomas Lindae |
lsp: tuned;
|
changeset |
files
|
| Sun, 30 Jun 2024 15:32:45 +0200 |
Thomas Lindae |
lsp: removed code that is never run;
|
changeset |
files
|
| Sun, 30 Jun 2024 15:32:39 +0200 |
Thomas Lindae |
lsp: created distinction for unicode symbols setting between output and edits and clarified output text functions;
|
changeset |
files
|
| Sun, 30 Jun 2024 15:32:32 +0200 |
Thomas Lindae |
clarified PIDE/line range conversions;
|
changeset |
files
|
| Sun, 30 Jun 2024 15:32:26 +0200 |
Thomas Lindae |
lsp: refactored conversion from Decoration_List to JSON;
|
changeset |
files
|
| Sun, 30 Jun 2024 15:32:19 +0200 |
Thomas Lindae |
lsp: tuned pretty_text_panel;
|
changeset |
files
|
| Sun, 30 Jun 2024 15:32:12 +0200 |
Thomas Lindae |
lsp: removed output_pretty_panel function as its logic is now in pretty_text_panel;
|
changeset |
files
|
| Sun, 30 Jun 2024 15:31:52 +0200 |
Thomas Lindae |
vscode: added more relevant options;
|
changeset |
files
|
| Fri, 14 Jun 2024 10:21:47 +0200 |
Thomas Lindae |
lsp: converted state panel to use a pretty text panel;
|
changeset |
files
|
| Fri, 14 Jun 2024 10:21:28 +0200 |
Thomas Lindae |
lsp: converted dynamic output to use a pretty text panel;
|
changeset |
files
|
| Fri, 14 Jun 2024 10:21:03 +0200 |
Thomas Lindae |
lsp: added Pretty_Text_Panel module;
|
changeset |
files
|
| Wed, 12 Jun 2024 21:26:31 +0200 |
Thomas Lindae |
vscode: added relevant isabelle options to vscode settings;
|
changeset |
files
|
| Wed, 12 Jun 2024 21:14:41 +0200 |
Thomas Lindae |
vscode: indent;
|
changeset |
files
|
| Wed, 12 Jun 2024 21:22:01 +0200 |
Thomas Lindae |
lsp: extracted panel content generation logic;
|
changeset |
files
|
| Wed, 12 Jun 2024 20:54:11 +0200 |
Thomas Lindae |
vscode: added all fonts to extension;
|
changeset |
files
|
| Wed, 12 Jun 2024 20:44:10 +0200 |
Thomas Lindae |
added vscode options tag;
|
changeset |
files
|
| Thu, 30 May 2024 02:43:29 +0200 |
Thomas Lindae |
vscode: tuned;
|
changeset |
files
|
| Thu, 30 May 2024 02:43:24 +0200 |
Thomas Lindae |
lsp: refactored non-html dynamic/state output;
|
changeset |
files
|
| Mon, 27 May 2024 13:21:15 +0200 |
Thomas Lindae |
vscode: reduced how often symbol width gets measured;
|
changeset |
files
|
| Mon, 27 May 2024 13:20:31 +0200 |
Thomas Lindae |
vscode: IsabelleDejaVuSansMono for state and output panel;
|
changeset |
files
|
| Mon, 27 May 2024 13:18:29 +0200 |
Thomas Lindae |
vscode: added decoration request on file switch;
|
changeset |
files
|
| Mon, 27 May 2024 13:17:09 +0200 |
Thomas Lindae |
lsp: added decoration_request notification;
|
changeset |
files
|
| Thu, 16 May 2024 11:59:33 +0200 |
Thomas Lindae |
lsp: added decorations to state updates;
|
changeset |
files
|
| Thu, 16 May 2024 11:59:06 +0200 |
Thomas Lindae |
lsp: added delay to dynamic_output updates after a set_margin;
|
changeset |
files
|
| Wed, 15 May 2024 17:04:22 +0200 |
Thomas Lindae |
lsp: added conversion of symbols for dynamic output so that decoration ranges consider vscode_unicode_symbols setting;
|
changeset |
files
|
| Wed, 15 May 2024 16:54:39 +0200 |
Thomas Lindae |
lsp: unified PIDE/decorations and dynamic output decorations format;
|
changeset |
files
|
| Wed, 15 May 2024 00:11:34 +0200 |
Thomas Lindae |
vscode: changed test_string to "mix" to be consistent with jEdit;
|
changeset |
files
|
| Thu, 16 May 2024 12:00:05 +0200 |
Thomas Lindae |
lsp: added decorations to dynamic output;
|
changeset |
files
|
| Thu, 09 May 2024 22:24:19 +0200 |
Thomas Lindae |
lsp: force update after state_set_margin;
|
changeset |
files
|
| Thu, 30 May 2024 02:45:01 +0200 |
Thomas Lindae |
vscode: added dynamic and state output set margin messages to vscode extension;
|
changeset |
files
|
| Sun, 30 Jun 2024 15:29:44 +0200 |
Thomas Lindae |
lsp: made margins synchronized;
|
changeset |
files
|
| Fri, 03 May 2024 20:13:48 +0200 |
Thomas Lindae |
lsp: added separation for non-html output and state;
|
changeset |
files
|
| Fri, 03 May 2024 20:11:41 +0200 |
Thomas Lindae |
lsp: tuned;
|
changeset |
files
|
| Fri, 03 May 2024 11:10:58 +0200 |
Thomas Lindae |
lsp: clarified preview_request;
|
changeset |
files
|
| Thu, 09 May 2024 23:05:10 +0200 |
Thomas Lindae |
lsp: added Symbols_Request;
|
changeset |
files
|
| Thu, 09 May 2024 22:22:44 +0200 |
Thomas Lindae |
lsp: added Output_Set_Margin and State_Set_Margin Notifications;
|
changeset |
files
|
| Mon, 01 Jul 2024 18:48:26 +0200 |
Thomas Lindae |
lsp: changed State_Init notification into a request and removed State_Init_Response;
|
changeset |
files
|
| Wed, 01 May 2024 19:09:26 +0200 |
Thomas Lindae |
lsp: tuned;
|
changeset |
files
|
| Thu, 30 May 2024 02:45:24 +0200 |
Thomas Lindae |
lsp: updated ErrorCodes;
|
changeset |
files
|
| Wed, 01 May 2024 12:34:53 +0200 |
Thomas Lindae |
lsp: added State and Dynamic Output html_output and margin handling;
|
changeset |
files
|
| Wed, 01 May 2024 12:30:53 +0200 |
Thomas Lindae |
lsp: added vscode_html_output option;
|
changeset |
files
|
| Wed, 01 May 2024 11:12:59 +0200 |
Thomas Lindae |
tuned formatting;
|
changeset |
files
|
| Wed, 24 Apr 2024 18:49:43 +0200 |
Thomas Lindae |
lsp: partially revert c0388fbd8096 to get decorations for all keywords;
|
changeset |
files
|
| Wed, 24 Apr 2024 18:48:24 +0200 |
Thomas Lindae |
lsp: added State_Init_Response message;
|
changeset |
files
|
| Thu, 30 May 2024 02:43:16 +0200 |
Thomas Lindae |
lsp: removed change_document normalization because it causes desyncs;
|
changeset |
files
|
| Mon, 30 Sep 2024 20:30:59 +0200 |
wenzelm |
clarified inner-syntax markup, notably for enumerations: prefer "notation=mixfix" over "entity" via 'syntax_consts' (see also 70076ba563d2);
|
changeset |
files
|
| Mon, 30 Sep 2024 13:00:42 +0200 |
wenzelm |
less markup: prefer "notatation" over "entity";
|
changeset |
files
|
| Mon, 30 Sep 2024 12:59:50 +0200 |
wenzelm |
clarify comparison of output: ignore token positions, which are somewhat accidental;
|
changeset |
files
|
| Mon, 30 Sep 2024 11:42:52 +0200 |
wenzelm |
clarified order of markup: more uniform input vs. output;
|
changeset |
files
|
| Mon, 30 Sep 2024 10:50:33 +0200 |
wenzelm |
misc tuning;
|
changeset |
files
|
| Mon, 30 Sep 2024 10:46:26 +0200 |
wenzelm |
clarified parse tree: always provide root node;
|
changeset |
files
|
| Mon, 30 Sep 2024 10:44:25 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Sun, 29 Sep 2024 22:47:14 +0200 |
wenzelm |
tuned markup;
|
changeset |
files
|
| Sun, 29 Sep 2024 21:57:47 +0200 |
wenzelm |
clarified markup: avoid conflict of "notation" with "entity", e.g. in "[x,y,z]" without spaces;
|
changeset |
files
|
| Sun, 29 Sep 2024 21:40:37 +0200 |
wenzelm |
more flexible command syntax;
|
changeset |
files
|
| Sun, 29 Sep 2024 21:20:36 +0200 |
wenzelm |
less markup (amending 07ad0b407d38): const = "" is mainly for parentheses syntax -- avoid entity_markup here;
|
changeset |
files
|
| Sun, 29 Sep 2024 21:16:17 +0200 |
wenzelm |
more markup reports: notably "notation=..." within pretty blocks;
|
changeset |
files
|
| Sun, 29 Sep 2024 21:13:17 +0200 |
wenzelm |
more parse tree positions;
|
changeset |
files
|
| Sun, 29 Sep 2024 21:03:28 +0200 |
wenzelm |
more operations;
|
changeset |
files
|
| Sun, 29 Sep 2024 20:11:28 +0200 |
wenzelm |
clarified order for 'print_syntax' command;
|
changeset |
files
|
| Sun, 29 Sep 2024 19:51:23 +0200 |
wenzelm |
more accurate parse tree: retain all tokens (and thus positions);
|
changeset |
files
|
| Sun, 29 Sep 2024 19:45:38 +0200 |
wenzelm |
more thorough markup reports (amending 0c6a600c8939 and 7f9e8516ca05): descend into vacuous nodes;
|
changeset |
files
|
| Sun, 29 Sep 2024 15:58:28 +0200 |
wenzelm |
clarified comparison: prefer authentic nonterminal context, instead of somewhat accidental "const";
|
changeset |
files
|
| Sun, 29 Sep 2024 15:24:17 +0200 |
wenzelm |
more detailed parse tree: retain nonterminal context as well;
|
changeset |
files
|
| Sun, 29 Sep 2024 15:08:38 +0200 |
wenzelm |
clarified persistent data;
|
changeset |
files
|
| Sun, 29 Sep 2024 15:00:20 +0200 |
wenzelm |
clarified input and output: support markup blocks via Bg/En;
|
changeset |
files
|
| Sun, 29 Sep 2024 14:55:49 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 29 Sep 2024 13:48:34 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 29 Sep 2024 12:09:49 +0200 |
wenzelm |
more operations;
|
changeset |
files
|
| Sun, 29 Sep 2024 11:18:34 +0200 |
wenzelm |
clarified output: count Tip entries;
|
changeset |
files
|
| Sun, 29 Sep 2024 11:08:43 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Sat, 28 Sep 2024 23:23:30 +0200 |
wenzelm |
tuned whitespace;
|
changeset |
files
|
| Sat, 28 Sep 2024 21:16:01 +0200 |
wenzelm |
clarified signature: more explicit type "output";
|
changeset |
files
|
| Sat, 28 Sep 2024 20:28:11 +0200 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Sat, 28 Sep 2024 17:11:51 +0200 |
wenzelm |
tuned: more uniform;
|
changeset |
files
|
| Sat, 28 Sep 2024 16:58:04 +0200 |
wenzelm |
tuned: more uniform;
|
changeset |
files
|
| Sat, 28 Sep 2024 16:19:53 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 28 Sep 2024 16:11:30 +0200 |
wenzelm |
minor performance tuning;
|
changeset |
files
|
| Sat, 28 Sep 2024 16:07:46 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 28 Sep 2024 15:58:09 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 28 Sep 2024 15:41:51 +0200 |
wenzelm |
minor performance tuning;
|
changeset |
files
|
| Fri, 27 Sep 2024 23:47:45 +0200 |
wenzelm |
partial revert of d97fdabd9e2b, to build old documentation more reliably;
|
changeset |
files
|
| Fri, 27 Sep 2024 22:44:30 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Fri, 27 Sep 2024 22:36:00 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Fri, 27 Sep 2024 22:28:46 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Fri, 27 Sep 2024 22:14:40 +0200 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Fri, 27 Sep 2024 22:08:54 +0200 |
wenzelm |
minor performance tuning: proper table for parsetree list;
|
changeset |
files
|
| Fri, 27 Sep 2024 20:29:38 +0200 |
wenzelm |
unused (see 954e9d6782ea);
|
changeset |
files
|
| Fri, 27 Sep 2024 20:19:38 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 27 Sep 2024 20:12:48 +0200 |
wenzelm |
unused (see 7c1e73540990);
|
changeset |
files
|
| Fri, 27 Sep 2024 20:09:54 +0200 |
wenzelm |
minor performance tuning (NB: order of prods / states does not matter);
|
changeset |
files
|
| Fri, 27 Sep 2024 18:46:58 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 27 Sep 2024 16:52:43 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 27 Sep 2024 14:22:06 +0200 |
wenzelm |
tuned comments;
|
changeset |
files
|
| Fri, 27 Sep 2024 13:52:16 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 27 Sep 2024 12:52:55 +0200 |
wenzelm |
pro-forma support for markup blocks, without any change of result yet;
|
changeset |
files
|
| Fri, 27 Sep 2024 11:14:38 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 26 Sep 2024 23:04:01 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Thu, 26 Sep 2024 21:55:46 +0200 |
wenzelm |
proper 'no_syntax' declarations (amending 8e72f55295fd);
|
changeset |
files
|
| Thu, 26 Sep 2024 11:41:51 +0200 |
wenzelm |
tuned, following make_symbs in src/Pure/Syntax/printer.ML;
|
changeset |
files
|
| Thu, 26 Sep 2024 11:31:43 +0200 |
wenzelm |
clarified use of Lexicon.dummy;
|
changeset |
files
|
| Thu, 26 Sep 2024 11:01:41 +0200 |
wenzelm |
unused (see 584828fa7a97);
|
changeset |
files
|
| Thu, 26 Sep 2024 10:51:36 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 26 Sep 2024 00:06:00 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 25 Sep 2024 23:34:31 +0200 |
wenzelm |
tuned: prefer ML over prose;
|
changeset |
files
|
| Wed, 25 Sep 2024 17:45:15 +0200 |
wenzelm |
eliminated redundant nt_count: rely on Symtab.size;
|
changeset |
files
|
| Wed, 25 Sep 2024 15:06:12 +0200 |
wenzelm |
eliminate unused prod_count (see also 7afca3218b65);
|
changeset |
files
|
| Wed, 25 Sep 2024 14:45:19 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 25 Sep 2024 13:32:52 +0200 |
wenzelm |
more markup;
|
changeset |
files
|
| Wed, 25 Sep 2024 13:30:04 +0200 |
wenzelm |
minor performance tuning: prefer static values;
|
changeset |
files
|
| Wed, 25 Sep 2024 13:20:36 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 25 Sep 2024 13:20:24 +0200 |
wenzelm |
more markup;
|
changeset |
files
|
| Wed, 25 Sep 2024 12:59:43 +0200 |
wenzelm |
clarified persistent datatype: more direct literal_markup, which also serves as a flag;
|
changeset |
files
|
| Wed, 25 Sep 2024 10:48:16 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Wed, 25 Sep 2024 10:38:46 +0200 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Fri, 23 Aug 2024 15:30:09 +0200 |
Fabian Huch |
add comments to rendering, e.g. to collect them from build database;
|
changeset |
files
|
| Thu, 26 Sep 2024 14:44:37 +0100 |
paulson |
To tiny but maybe useful lemmas (moved in from the AFP, Word_Lib)
|
changeset |
files
|
| Tue, 24 Sep 2024 21:41:01 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 24 Sep 2024 21:31:20 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 24 Sep 2024 21:24:44 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 24 Sep 2024 20:10:11 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 24 Sep 2024 19:58:24 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 24 Sep 2024 18:25:36 +0200 |
wenzelm |
minor performance tuning for blocks without markup;
|
changeset |
files
|
| Tue, 24 Sep 2024 18:17:39 +0200 |
wenzelm |
more markup <expression kind="item"> in Isabelle/Scala, with pro-forma Markup_Kind.setup in Isabelle/ML;
|
changeset |
files
|
| Tue, 24 Sep 2024 17:57:42 +0200 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Tue, 24 Sep 2024 17:41:05 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 24 Sep 2024 17:35:24 +0200 |
wenzelm |
minor performance tuning: more direct blocks without markup;
|
changeset |
files
|
| Tue, 24 Sep 2024 17:31:12 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 24 Sep 2024 17:27:56 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Mon, 23 Sep 2024 22:33:37 +0200 |
wenzelm |
proper 'no_syntax' (amending 8e72f55295fd);
|
changeset |
files
|
| Mon, 23 Sep 2024 21:09:23 +0200 |
wenzelm |
more inner syntax markup: HOL;
|
changeset |
files
|
| Mon, 23 Sep 2024 15:01:10 +0200 |
wenzelm |
misc tuning and clarification;
|
changeset |
files
|
| Mon, 23 Sep 2024 13:32:38 +0200 |
wenzelm |
standardize mixfix annotations via "isabelle update -u mixfix_cartouches -l Pure HOL" --- to simplify systematic editing;
|
changeset |
files
|
| Mon, 23 Sep 2024 12:59:10 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 23 Sep 2024 11:36:03 +0200 |
wenzelm |
minor performance tuning: more concise tuples;
|
changeset |
files
|
| Mon, 23 Sep 2024 11:08:30 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 23 Sep 2024 10:56:25 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 23 Sep 2024 10:45:05 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 22 Sep 2024 18:47:43 +0200 |
wenzelm |
misc tuning and clarification;
|
changeset |
files
|
| Sun, 22 Sep 2024 17:40:28 +0200 |
wenzelm |
more antiquotations;
|
changeset |
files
|
| Sun, 22 Sep 2024 16:18:49 +0200 |
wenzelm |
tuned comments;
|
changeset |
files
|
| Sun, 22 Sep 2024 16:12:15 +0200 |
wenzelm |
more specific markup for "judgment";
|
changeset |
files
|
| Sun, 22 Sep 2024 16:04:44 +0200 |
wenzelm |
remove specific support for "expression" block markup: prefer "notation";
|
changeset |
files
|
| Sun, 22 Sep 2024 15:58:55 +0200 |
wenzelm |
clarified inner syntax markup: use "notation" uniformly;
|
changeset |
files
|
| Sun, 22 Sep 2024 15:46:19 +0200 |
wenzelm |
more uniform treatment of Markup.notation and Markup.expression: manage kinds via context;
|
changeset |
files
|
| Sun, 22 Sep 2024 14:41:34 +0200 |
wenzelm |
clarified modules and signature;
|
changeset |
files
|
| Sun, 22 Sep 2024 14:33:03 +0200 |
wenzelm |
proper fbreaks (amending 53f12ab896e6);
|
changeset |
files
|
| Fri, 20 Sep 2024 23:37:00 +0200 |
wenzelm |
more inner syntax markup: minor object-logics;
|
changeset |
files
|
| Fri, 20 Sep 2024 23:36:33 +0200 |
wenzelm |
more inner syntax markup: Pure;
|
changeset |
files
|
| Fri, 20 Sep 2024 21:34:09 +0200 |
wenzelm |
more markup elements;
|
changeset |
files
|
| Fri, 20 Sep 2024 19:51:08 +0200 |
wenzelm |
standardize mixfix annotations via "isabelle update -a -u mixfix_cartouches" --- to simplify systematic editing;
|
changeset |
files
|
| Fri, 20 Sep 2024 19:07:10 +0200 |
wenzelm |
proper Haskell setup, following 406a85a25189;
|
changeset |
files
|
| Fri, 20 Sep 2024 18:09:04 +0200 |
wenzelm |
support more markup elements;
|
changeset |
files
|
| Fri, 20 Sep 2024 15:35:16 +0200 |
wenzelm |
block markup for specific notation, notably infix and binder;
|
changeset |
files
|
| Fri, 20 Sep 2024 14:28:13 +0200 |
wenzelm |
clarified signature: more explicit operations;
|
changeset |
files
|
| Fri, 20 Sep 2024 13:30:55 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 20 Sep 2024 11:19:23 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 20 Sep 2024 11:10:04 +0200 |
wenzelm |
no need to suppress positions (see ff3b8e4079bd) thanks to Context_Position.set_visible false (see 5328d67ec647);
|
changeset |
files
|
| Fri, 20 Sep 2024 11:04:35 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 19 Sep 2024 21:13:26 +0200 |
wenzelm |
support for Markup.expression properties in pretty-blocks;
|
changeset |
files
|
| Thu, 19 Sep 2024 20:56:47 +0200 |
wenzelm |
more positions;
|
changeset |
files
|
| Thu, 19 Sep 2024 20:38:34 +0200 |
wenzelm |
more operations;
|
changeset |
files
|
| Thu, 19 Sep 2024 20:38:19 +0200 |
wenzelm |
more operations;
|
changeset |
files
|
| Thu, 19 Sep 2024 12:41:02 +0200 |
wenzelm |
minor performance tuning: avoid vacuous update of context;
|
changeset |
files
|
| Thu, 19 Sep 2024 12:10:17 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 19 Sep 2024 12:08:56 +0200 |
wenzelm |
proper Context_Position.report, following 5328d67ec647;
|
changeset |
files
|
| Tue, 17 Sep 2024 18:49:46 +0200 |
wenzelm |
more operations;
|
changeset |
files
|
| Tue, 17 Sep 2024 17:51:55 +0200 |
wenzelm |
more explicit context for syn_ext/mixfix operations, but it often degenerates to background theory;
|
changeset |
files
|
| Tue, 17 Sep 2024 17:05:37 +0200 |
wenzelm |
obsolete --- superseded by Local_Theory.syntax_cmd;
|
changeset |
files
|
| Tue, 17 Sep 2024 11:32:11 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 17 Sep 2024 11:14:25 +0200 |
wenzelm |
unused (see 39261908e12f);
|
changeset |
files
|
| Tue, 17 Sep 2024 11:06:11 +0200 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Tue, 17 Sep 2024 11:00:03 +0200 |
wenzelm |
tuned comments;
|
changeset |
files
|
| Tue, 17 Sep 2024 10:47:08 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 16 Sep 2024 20:44:46 +0200 |
wenzelm |
more detailed markup;
|
changeset |
files
|
| Mon, 16 Sep 2024 19:58:28 +0200 |
wenzelm |
more formal Markup.expression;
|
changeset |
files
|
| Mon, 16 Sep 2024 19:36:20 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 16 Sep 2024 18:59:39 +0200 |
wenzelm |
clarified name space: no theory qualifier here --- treat like global datatype constructors;
|
changeset |
files
|
| Mon, 16 Sep 2024 15:49:36 +0200 |
wenzelm |
discontinued "isabelle build -k": superseded by admin-tool "isabelle check_keywords";
|
changeset |
files
|
| Mon, 16 Sep 2024 15:39:35 +0200 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Mon, 16 Sep 2024 14:03:25 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Mon, 16 Sep 2024 13:53:43 +0200 |
wenzelm |
obsolete (see also b93cc7d73431);
|
changeset |
files
|
| Sun, 15 Sep 2024 16:45:13 +0200 |
wenzelm |
performance tuning: cache for highly redundant markup (types and sorts);
|
changeset |
files
|
| Sun, 15 Sep 2024 14:56:33 +0200 |
wenzelm |
more operations;
|
changeset |
files
|
| Sun, 15 Sep 2024 14:21:31 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 15 Sep 2024 14:06:06 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 15 Sep 2024 13:47:25 +0200 |
wenzelm |
tuned signature and module structure;
|
changeset |
files
|
| Fri, 13 Sep 2024 19:13:53 +0200 |
wenzelm |
less ambitious Bytes.chunk_size for potentially more stable Poly/ML GC (see f0d8f659b19a, but also java.io.InputStream.DEFAULT_BUFFER_SIZE);
|
changeset |
files
|
| Thu, 12 Sep 2024 20:15:28 +0200 |
wenzelm |
tuned signature: more operations;
|
changeset |
files
|
| Thu, 12 Sep 2024 19:52:01 +0200 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Thu, 12 Sep 2024 19:46:08 +0200 |
wenzelm |
prefer Pretty.pure_string_of to produce output without markup, instead of cleaning output afterwards;
|
changeset |
files
|
| Thu, 12 Sep 2024 15:09:07 +0200 |
wenzelm |
clarified signature: more explicit operations;
|
changeset |
files
|
| Thu, 12 Sep 2024 14:42:04 +0200 |
wenzelm |
tuned: trim message before formatting;
|
changeset |
files
|
| Thu, 12 Sep 2024 14:38:19 +0200 |
wenzelm |
tuned signature: more operations;
|
changeset |
files
|
| Thu, 12 Sep 2024 14:24:36 +0200 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Thu, 12 Sep 2024 13:13:59 +0200 |
wenzelm |
clarified print_mode (again, amending 9de19e3a7231): support e.g. 'thm ("") symmetric' for formatting in ML and without markup;
|
changeset |
files
|
| Thu, 12 Sep 2024 13:10:36 +0200 |
wenzelm |
more robust reports: ensure that markup is actually present;
|
changeset |
files
|
| Thu, 12 Sep 2024 13:09:26 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Wed, 11 Sep 2024 23:26:25 +0200 |
wenzelm |
clarified internal tool output: prefer Pretty.pure_string_of over manipulation of print_mode;
|
changeset |
files
|
| Wed, 11 Sep 2024 23:07:18 +0200 |
wenzelm |
unused;
|
changeset |
files
|
| Wed, 11 Sep 2024 22:56:42 +0200 |
wenzelm |
misc tuning and clarification (see also 86a31308a8e1);
|
changeset |
files
|
| Wed, 11 Sep 2024 22:28:42 +0200 |
wenzelm |
tuned signature: more operations;
|
changeset |
files
|
| Wed, 11 Sep 2024 21:41:33 +0200 |
wenzelm |
clarified modules;
|
changeset |
files
|
| Wed, 11 Sep 2024 21:25:15 +0200 |
wenzelm |
dismantle print_mode operations for Markup/Pretty: hardwired check of "print_mode_active Print_Mode.PIDE";
|
changeset |
files
|
| Wed, 11 Sep 2024 20:45:17 +0200 |
wenzelm |
clarified YXML bootstrap;
|
changeset |
files
|
| Wed, 11 Sep 2024 20:06:12 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 11 Sep 2024 20:05:09 +0200 |
wenzelm |
more robust: global ML name space for markup elements;
|
changeset |
files
|
| Wed, 11 Sep 2024 19:59:10 +0200 |
wenzelm |
clarified properties;
|
changeset |
files
|
| Wed, 11 Sep 2024 19:53:35 +0200 |
wenzelm |
clarified signature and modules;
|
changeset |
files
|
| Wed, 11 Sep 2024 19:35:21 +0200 |
wenzelm |
further clarification of print_mode: PIDE markup depends on "isabelle_process" alone, Latex is stateless;
|
changeset |
files
|
| Wed, 11 Sep 2024 17:00:02 +0200 |
wenzelm |
misc tuning and clarification;
|
changeset |
files
|
| Wed, 11 Sep 2024 15:36:14 +0200 |
wenzelm |
minor performance tuning, notably for Bytes.add (e.g. YXML output);
|
changeset |
files
|
| Wed, 11 Sep 2024 12:46:56 +0200 |
wenzelm |
revert 90f6e541e926, which has become pointless thanks to df85df6315af;
|
changeset |
files
|
| Wed, 11 Sep 2024 12:32:11 +0200 |
wenzelm |
clarified signature and modules;
|
changeset |
files
|
| Wed, 11 Sep 2024 12:18:29 +0200 |
wenzelm |
clarified files;
|
changeset |
files
|
| Wed, 11 Sep 2024 12:11:47 +0200 |
wenzelm |
drop pointless print_mode operations Output.output / Output.escape;
|
changeset |
files
|
| Tue, 10 Sep 2024 20:36:01 +0200 |
wenzelm |
clarified signature: prefer explicit type Bytes.T;
|
changeset |
files
|
| Tue, 10 Sep 2024 20:06:51 +0200 |
wenzelm |
clarified signature, roughly following Isabelle/Scala;
|
changeset |
files
|
| Tue, 10 Sep 2024 19:57:45 +0200 |
wenzelm |
clarified print mode "latex": no longer impact Output/Markup/Pretty operations;
|
changeset |
files
|
| Tue, 10 Sep 2024 16:06:38 +0200 |
wenzelm |
tuned comments, following Isabelle/ML;
|
changeset |
files
|
| Tue, 10 Sep 2024 16:03:42 +0200 |
wenzelm |
tuned module structure;
|
changeset |
files
|
| Tue, 10 Sep 2024 15:35:51 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 10 Sep 2024 14:53:04 +0200 |
wenzelm |
clarified unbreakable latex output: Pretty.unformatted and (Pretty.string_of o Pretty.unbreakable) should coincide, but are produced by quite different means;
|
changeset |
files
|
| Tue, 10 Sep 2024 12:34:32 +0200 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Tue, 10 Sep 2024 12:22:24 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Tue, 10 Sep 2024 12:05:37 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 09 Sep 2024 23:50:58 +0200 |
wenzelm |
minor performance tuning, following Isabelle/Scala;
|
changeset |
files
|
| Mon, 09 Sep 2024 23:47:08 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 09 Sep 2024 23:45:45 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Mon, 09 Sep 2024 22:59:51 +0200 |
wenzelm |
more scalable;
|
changeset |
files
|
| Mon, 09 Sep 2024 22:59:41 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 09 Sep 2024 22:40:33 +0200 |
wenzelm |
eliminate print mode "code_presentation" thanks to value-oriented Pretty.T operations;
|
changeset |
files
|
| Mon, 09 Sep 2024 22:04:46 +0200 |
wenzelm |
NEWS: value-oriented Pretty.T;
|
changeset |
files
|
| Mon, 09 Sep 2024 21:54:41 +0200 |
wenzelm |
proper formal sections;
|
changeset |
files
|
| Mon, 09 Sep 2024 21:45:56 +0200 |
wenzelm |
tuned signature: more options;
|
changeset |
files
|
| Mon, 09 Sep 2024 21:32:11 +0200 |
wenzelm |
clarified Pretty.markup_block: use value-oriented YXML.output_markup, with final re-interpretation via print_mode in output_tree;
|
changeset |
files
|
| Mon, 09 Sep 2024 21:23:28 +0200 |
wenzelm |
minor performance tuning;
|
changeset |
files
|
| Mon, 09 Sep 2024 19:51:16 +0200 |
wenzelm |
unused;
|
changeset |
files
|
| Mon, 09 Sep 2024 19:40:18 +0200 |
wenzelm |
prefer static YXML.output_markup_only (without print_mode): Output.status is only relevant for PIDE (with print_mode "isabelle_process");
|
changeset |
files
|
| Mon, 09 Sep 2024 19:00:53 +0200 |
wenzelm |
clarified signature: more explicit type output_ops: default via print_mode;
|
changeset |
files
|
| Mon, 09 Sep 2024 13:43:28 +0200 |
wenzelm |
discontinued unused global variable (see also following bf465f335e85);
|
changeset |
files
|
| Mon, 09 Sep 2024 11:41:31 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Mon, 09 Sep 2024 11:21:48 +0200 |
wenzelm |
clarified modules (see also ea7c2ee8a47a);
|
changeset |
files
|
| Mon, 09 Sep 2024 11:12:13 +0200 |
wenzelm |
clarified signature: more explicit type "ops";
|
changeset |
files
|
| Fri, 06 Sep 2024 20:31:20 +0200 |
wenzelm |
more thorough Protocol_Message.clean_output, following Isabelle/Scala;
|
changeset |
files
|
| Fri, 06 Sep 2024 19:17:29 +0200 |
wenzelm |
more accurate output, following 3f02bc5a5a03;
|
changeset |
files
|
| Fri, 06 Sep 2024 19:08:44 +0200 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Fri, 06 Sep 2024 15:59:48 +0200 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Fri, 06 Sep 2024 15:46:51 +0200 |
wenzelm |
misc tuning and clarification;
|
changeset |
files
|
| Fri, 06 Sep 2024 14:47:42 +0200 |
wenzelm |
proper signature (amending 0f820da558f9);
|
changeset |
files
|
| Fri, 06 Sep 2024 14:34:07 +0200 |
wenzelm |
more accurate output: observe depth as in "prune" operation;
|
changeset |
files
|
| Fri, 06 Sep 2024 13:57:06 +0200 |
wenzelm |
clarified signature, following 1f718be3608b: Pretty.str is now value-oriented;
|
changeset |
files
|
| Fri, 06 Sep 2024 13:49:43 +0200 |
wenzelm |
clarified signature and modules;
|
changeset |
files
|
| Fri, 06 Sep 2024 13:19:18 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 05 Sep 2024 21:16:53 +0200 |
wenzelm |
clarified Pretty.T vs. output tree (following Isabelle/Scala): Output.output_width (via print_mode) happens during formatting, instead of construction;
|
changeset |
files
|
| Thu, 05 Sep 2024 17:39:45 +0200 |
wenzelm |
clarified signature: type ML_Pretty.pretty coincides with PolyML.pretty;
|
changeset |
files
|
| Wed, 04 Sep 2024 16:21:52 +0200 |
wenzelm |
clarified signature (see also 8bef51521f21);
|
changeset |
files
|
| Wed, 04 Sep 2024 13:55:57 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Wed, 04 Sep 2024 12:50:52 +0200 |
wenzelm |
more accurate Default_Metric;
|
changeset |
files
|
| Mon, 02 Sep 2024 22:41:23 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Mon, 02 Sep 2024 22:00:53 +0200 |
wenzelm |
clarified output_spaces, based on Output.output_width;
|
changeset |
files
|
| Mon, 02 Sep 2024 20:54:00 +0200 |
wenzelm |
clarified modules: enable pretty.ML to use XML/YXML more directly;
|
changeset |
files
|
| Mon, 02 Sep 2024 20:12:52 +0200 |
wenzelm |
removed unused operation (reverting 4660b0409096);
|
changeset |
files
|
| Mon, 02 Sep 2024 15:23:12 +0200 |
wenzelm |
clarified modules;
|
changeset |
files
|
| Mon, 02 Sep 2024 14:36:35 +0200 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Mon, 02 Sep 2024 13:57:17 +0200 |
wenzelm |
tuned: prefer Symbol.spaces;
|
changeset |
files
|
| Mon, 02 Sep 2024 13:42:38 +0200 |
wenzelm |
tuned whitespace;
|
changeset |
files
|
| Mon, 02 Sep 2024 13:41:40 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 01 Sep 2024 22:59:11 +0200 |
wenzelm |
more NEWS;
|
changeset |
files
|
| Sun, 01 Sep 2024 19:35:30 +0200 |
wenzelm |
proper string syntax (amending 70076ba563d2);
|
changeset |
files
|
| Sat, 31 Aug 2024 16:01:36 +0200 |
wenzelm |
avoid redundant XML.blob: Bytes.contents consist of larger chunks;
|
changeset |
files
|
| Sat, 31 Aug 2024 16:00:16 +0200 |
wenzelm |
minor performance tuning: avoid many small strings, notably in File_Stream.output;
|
changeset |
files
|
| Fri, 30 Aug 2024 17:00:21 +0100 |
paulson |
A bit of tidying
|
changeset |
files
|
| Fri, 30 Aug 2024 10:44:48 +0100 |
paulson |
merged
|
changeset |
files
|
| Fri, 30 Aug 2024 10:16:48 +0100 |
paulson |
More tidying of old proofs
|
changeset |
files
|
| Thu, 29 Aug 2024 17:47:29 +0200 |
wenzelm |
more scalable pretty printing: avoid exception String.Size at command "value" (line 33 of "$AFP/Iptables_Semantics/Examples/SQRL_Shorewall/Analyze_SQRL_Shorewall.thy") in AFP/c69af9cd3390;
|
changeset |
files
|
| Thu, 29 Aug 2024 11:43:14 +0200 |
wenzelm |
more specific "args" syntax, to support more markup for syntax consts;
|
changeset |
files
|
| Thu, 29 Aug 2024 11:39:50 +0200 |
wenzelm |
more direct notation;
|
changeset |
files
|
| Wed, 28 Aug 2024 22:54:45 +0200 |
wenzelm |
more specific "args" syntax, to support more markup for syntax consts;
|
changeset |
files
|
| Wed, 28 Aug 2024 20:46:45 +0200 |
wenzelm |
proper definition to avoid failure of HOL-Codegenerator_Test (amending 3d9e7746d9db);
|
changeset |
files
|
| Wed, 28 Aug 2024 19:40:07 +0200 |
wenzelm |
further attempts at markup for monad notation;
|
changeset |
files
|
| Wed, 28 Aug 2024 16:46:33 +0200 |
wenzelm |
more markup for syntax consts;
|
changeset |
files
|
| Tue, 27 Aug 2024 13:53:18 +0200 |
Fabian Huch |
stop web server on close;
|
changeset |
files
|
| Tue, 27 Aug 2024 13:44:23 +0200 |
Fabian Huch |
better results for terminated jobs;
|
changeset |
files
|
| Tue, 27 Aug 2024 13:12:10 +0200 |
Fabian Huch |
more robust: clean up unfinished jobs on init, e.g. if build_manager process was forcefully terminated;
|
changeset |
files
|
| Tue, 27 Aug 2024 12:57:49 +0200 |
Fabian Huch |
manage runner state properly (amending be4c1fbccfe8);
|
changeset |
files
|
| Mon, 26 Aug 2024 22:14:19 +0100 |
paulson |
merged
|
changeset |
files
|
| Mon, 26 Aug 2024 21:59:35 +0100 |
paulson |
More tidying of old proofs
|
changeset |
files
|
| Mon, 26 Aug 2024 22:52:27 +0200 |
nipkow |
more precise bound
|
changeset |
files
|
| Mon, 26 Aug 2024 18:26:06 +0200 |
nipkow |
merged
|
changeset |
files
|
| Mon, 26 Aug 2024 18:26:00 +0200 |
nipkow |
get rid of manual T_f defs
|
changeset |
files
|
| Mon, 26 Aug 2024 13:15:34 +0200 |
wenzelm |
NEWS and documentation;
|
changeset |
files
|
| Sun, 25 Aug 2024 23:19:33 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Sun, 25 Aug 2024 22:54:56 +0200 |
wenzelm |
use nicer notation, following 783406dd051e;
|
changeset |
files
|
| Sun, 25 Aug 2024 21:27:25 +0100 |
paulson |
merged
|
changeset |
files
|
| Sun, 25 Aug 2024 17:24:42 +0100 |
paulson |
A bit more tidying
|
changeset |
files
|
| Sun, 25 Aug 2024 21:10:01 +0200 |
wenzelm |
more markup for syntax consts;
|
changeset |
files
|
| Sun, 25 Aug 2024 20:54:20 +0200 |
wenzelm |
clarified Syntax.is_const (after 43c4817375bf): exclude logical consts from 'syntax_consts' / 'syntax_types', e.g. relevant for @{syntax_const} antiquotation;
|
changeset |
files
|
| Sun, 25 Aug 2024 16:00:59 +0200 |
wenzelm |
use nicer notation, following 783406dd051e;
|
changeset |
files
|
| Sun, 25 Aug 2024 15:53:03 +0200 |
wenzelm |
proper translation for "_qprod", following "_qsum" (see also e14b89d6ef13 and fa7d27ef7e59);
|
changeset |
files
|
| Sun, 25 Aug 2024 15:40:07 +0200 |
wenzelm |
tuned: prefer notation for Pure.type;
|
changeset |
files
|
| Sun, 25 Aug 2024 15:16:32 +0200 |
wenzelm |
tuned whitespace;
|
changeset |
files
|
| Sun, 25 Aug 2024 15:11:41 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 25 Aug 2024 15:07:22 +0200 |
wenzelm |
tuned, following be8c0e039a5e;
|
changeset |
files
|
| Sun, 25 Aug 2024 15:02:19 +0200 |
wenzelm |
more markup for syntax consts;
|
changeset |
files
|
| Sun, 25 Aug 2024 12:43:43 +0200 |
wenzelm |
proper flags (amending 1319c729c65d): abbrevs are allowed, free variables are disallowed;
|
changeset |
files
|
| Sat, 24 Aug 2024 23:44:05 +0100 |
paulson |
Some tidying
|
changeset |
files
|
| Sat, 24 Aug 2024 14:14:57 +0100 |
paulson |
merged
|
changeset |
files
|
| Sat, 24 Aug 2024 14:14:44 +0100 |
paulson |
Tidied some messy old proofs
|
changeset |
files
|
| Fri, 23 Aug 2024 23:16:53 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Fri, 23 Aug 2024 23:14:39 +0200 |
wenzelm |
more markup for syntax consts;
|
changeset |
files
|
| Fri, 23 Aug 2024 22:47:51 +0200 |
wenzelm |
more markup for syntax consts;
|
changeset |
files
|
| Fri, 23 Aug 2024 22:45:18 +0200 |
wenzelm |
clarified concrete syntax;
|
changeset |
files
|
| Fri, 23 Aug 2024 21:32:09 +0200 |
wenzelm |
more accurate markup (amending 43c4817375bf): only consider primitive syntax consts, avoid extra Markup.intensify e.g. due to "\<^const>Pure.all_binder";
|
changeset |
files
|
| Fri, 23 Aug 2024 20:45:54 +0200 |
wenzelm |
more concrete syntax and more checks;
|
changeset |
files
|
| Fri, 23 Aug 2024 20:21:04 +0200 |
wenzelm |
clarified signature: more operations;
|
changeset |
files
|
| Fri, 23 Aug 2024 18:38:44 +0200 |
wenzelm |
support for syntax const dependencies, with minimal integrity checks;
|
changeset |
files
|
| Fri, 23 Aug 2024 15:44:31 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 23 Aug 2024 15:42:30 +0200 |
wenzelm |
clarified markup: more uniform treatment of parse/print phase;
|
changeset |
files
|
| Fri, 23 Aug 2024 14:59:16 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 23 Aug 2024 14:56:33 +0200 |
wenzelm |
clarified markup: more uniform;
|
changeset |
files
|
| Fri, 23 Aug 2024 14:41:45 +0200 |
wenzelm |
tuned signature: separate markup vs. extern;
|
changeset |
files
|
| Fri, 23 Aug 2024 13:28:01 +0200 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Thu, 22 Aug 2024 17:12:32 +0200 |
wenzelm |
tuned: prefer configuration options via context;
|
changeset |
files
|
| Thu, 22 Aug 2024 16:04:06 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 22 Aug 2024 15:57:30 +0200 |
wenzelm |
tuned signature: more operations;
|
changeset |
files
|
| Fri, 23 Aug 2024 18:40:12 +0200 |
nipkow |
tuned comments
|
changeset |
files
|
| Thu, 22 Aug 2024 22:26:36 +0100 |
paulson |
merged
|
changeset |
files
|
| Thu, 22 Aug 2024 22:26:28 +0100 |
paulson |
Partial tidying of old proofs
|
changeset |
files
|
| Wed, 21 Aug 2024 20:41:16 +0200 |
nipkow |
merged
|
changeset |
files
|
| Wed, 21 Aug 2024 20:40:59 +0200 |
nipkow |
new version of time_fun that works for classes; define T_length automatically now
|
changeset |
files
|
| Wed, 21 Aug 2024 14:09:44 +0100 |
paulson |
merged
|
changeset |
files
|
| Fri, 09 Aug 2024 20:45:31 +0100 |
paulson |
revised/generalised some lemmas
|
changeset |
files
|
| Wed, 21 Aug 2024 13:33:19 +0200 |
Fabian Huch |
remove terminated jobs, even if futures do not complete;
|
changeset |
files
|
| Tue, 20 Aug 2024 17:28:51 +0200 |
Fabian Huch |
terminate jobs properly;
|
changeset |
files
|
| Sun, 18 Aug 2024 20:03:32 +0200 |
wenzelm |
clarified signature: eliminate clones;
|
changeset |
files
|
| Sun, 18 Aug 2024 19:37:32 +0200 |
wenzelm |
tuned: more antiquotations;
|
changeset |
files
|
| Sun, 18 Aug 2024 18:51:31 +0200 |
wenzelm |
tuned: more antiquotations;
|
changeset |
files
|
| Sun, 18 Aug 2024 18:08:16 +0200 |
wenzelm |
misc tuning;
|
changeset |
files
|
| Sun, 18 Aug 2024 16:46:32 +0200 |
wenzelm |
tuned: eliminate clone (with change of internal exceptions);
|
changeset |
files
|
| Sun, 18 Aug 2024 15:49:24 +0200 |
wenzelm |
tuned: more antiquotations;
|
changeset |
files
|
| Sun, 18 Aug 2024 15:41:55 +0200 |
wenzelm |
tuned comments and whitespace (see also 589645894305);
|
changeset |
files
|
| Sun, 18 Aug 2024 15:29:18 +0200 |
wenzelm |
tuned: more antiquotations;
|
changeset |
files
|
| Sun, 18 Aug 2024 15:29:03 +0200 |
wenzelm |
tuned: more antiquotations;
|
changeset |
files
|
| Sun, 18 Aug 2024 15:21:50 +0200 |
wenzelm |
proper const (see also 759bffe1d416 and b2800da9eb8a);
|
changeset |
files
|
| Sun, 18 Aug 2024 15:08:32 +0200 |
wenzelm |
tuned: inline constants;
|
changeset |
files
|
| Sun, 18 Aug 2024 14:49:23 +0200 |
wenzelm |
tuned: eliminate clone;
|
changeset |
files
|
| Sun, 18 Aug 2024 14:40:49 +0200 |
wenzelm |
tuned: more antiquotations;
|
changeset |
files
|
| Sun, 18 Aug 2024 14:22:21 +0200 |
wenzelm |
prefer host that is less likely to be down;
|
changeset |
files
|
| Thu, 15 Aug 2024 13:58:09 +0200 |
wenzelm |
adapt and activate congprocs examples, following the current Simplifier implementation;
|
changeset |
files
|
| Thu, 15 Aug 2024 13:47:09 +0200 |
wenzelm |
original Congproc_Ex.thy by Norbert Schirmer: still inactive;
|
changeset |
files
|
| Thu, 15 Aug 2024 13:45:48 +0200 |
wenzelm |
provide Simplifier.set_mksimps_context (roughly following Norbert Schirmer): allow update of context when premises are added to the local simpset;
|
changeset |
files
|
| Thu, 15 Aug 2024 12:43:17 +0200 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Thu, 15 Aug 2024 12:22:39 +0200 |
wenzelm |
more direct access to Simplifier.mk_cong, to avoid odd Simpdata.mk_meta_cong seen in the wild;
|
changeset |
files
|
| Thu, 15 Aug 2024 11:49:45 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 14 Aug 2024 21:23:22 +0200 |
wenzelm |
support for congprocs in the Simplifier, closely following Norbert Schirmer et-al, but with only one "simproc" name space and "simproc_setup" command / ML antiquotation;
|
changeset |
files
|
| Wed, 14 Aug 2024 18:59:49 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 14 Aug 2024 16:48:16 +0200 |
wenzelm |
tuned: anticipate congprocs;
|
changeset |
files
|
| Wed, 14 Aug 2024 15:30:29 +0200 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Wed, 14 Aug 2024 13:51:36 +0200 |
wenzelm |
tuned signature (again): anticipate different kinds of procs;
|
changeset |
files
|
| Wed, 14 Aug 2024 13:10:39 +0200 |
wenzelm |
clarified context data;
|
changeset |
files
|
| Tue, 13 Aug 2024 21:09:51 +0200 |
wenzelm |
tuned: prefer canonical argument order;
|
changeset |
files
|
| Tue, 13 Aug 2024 19:28:58 +0200 |
wenzelm |
tuned: more antiquotations;
|
changeset |
files
|
| Tue, 13 Aug 2024 18:53:24 +0200 |
wenzelm |
tuned: prefer canonical argument order;
|
changeset |
files
|
| Tue, 13 Aug 2024 18:31:40 +0200 |
wenzelm |
clarified signature: less redundant types;
|
changeset |
files
|
| Tue, 13 Aug 2024 16:01:05 +0200 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Tue, 13 Aug 2024 15:50:25 +0200 |
wenzelm |
unused (see d12c58e12c51);
|
changeset |
files
|
| Tue, 13 Aug 2024 15:42:55 +0200 |
wenzelm |
tuned signature: support more general procedures;
|
changeset |
files
|
| Sun, 11 Aug 2024 23:11:03 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Sun, 11 Aug 2024 20:20:05 +0200 |
wenzelm |
tuned: more antiquotations;
|
changeset |
files
|
| Sun, 11 Aug 2024 20:19:47 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 11 Aug 2024 14:45:56 +0200 |
wenzelm |
tuned: more antiquotations;
|
changeset |
files
|
| Sun, 11 Aug 2024 14:18:40 +0200 |
wenzelm |
tuned whitespace;
|
changeset |
files
|
| Sun, 11 Aug 2024 13:08:11 +0200 |
wenzelm |
more robust (amending 8f53fa93d5f0): R could be anything and Thm.instantiate' involves some type-checks, e.g. relevant for lemma fset_simps in theory Quotient_Examples.Quotient_FSet;
|
changeset |
files
|
| Sun, 11 Aug 2024 11:32:20 +0200 |
wenzelm |
tuned modules;
|
changeset |
files
|
| Sat, 10 Aug 2024 21:32:10 +0200 |
wenzelm |
misc tuning;
|
changeset |
files
|
| Sat, 10 Aug 2024 21:14:07 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 10 Aug 2024 21:13:37 +0200 |
wenzelm |
tuned: more antiquotations;
|
changeset |
files
|
| Sat, 10 Aug 2024 20:46:12 +0200 |
wenzelm |
misc tuning;
|
changeset |
files
|
| Sat, 10 Aug 2024 20:45:55 +0200 |
wenzelm |
misc tuning and clarification;
|
changeset |
files
|
| Sat, 10 Aug 2024 20:20:59 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 10 Aug 2024 20:20:52 +0200 |
wenzelm |
misc tuning and clarification: proper context, proper exception;
|
changeset |
files
|
| Sat, 10 Aug 2024 13:49:08 +0200 |
wenzelm |
tuned: eliminate odd clones;
|
changeset |
files
|
| Sat, 10 Aug 2024 13:42:27 +0200 |
wenzelm |
tuned: more antiquotations;
|
changeset |
files
|
| Sat, 10 Aug 2024 13:42:16 +0200 |
wenzelm |
unused;
|
changeset |
files
|
| Sat, 10 Aug 2024 12:26:17 +0200 |
wenzelm |
tuned: more antiquotations;
|
changeset |
files
|
| Sat, 10 Aug 2024 12:12:53 +0200 |
wenzelm |
tuned: more antiquotations;
|
changeset |
files
|
| Thu, 08 Aug 2024 22:49:40 +0200 |
wenzelm |
tuned: more antiquotations;
|
changeset |
files
|
| Thu, 08 Aug 2024 17:06:08 +0200 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Thu, 08 Aug 2024 16:23:30 +0200 |
wenzelm |
tuned signature: more operations;
|
changeset |
files
|
| Thu, 08 Aug 2024 16:21:48 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 08 Aug 2024 16:03:34 +0200 |
wenzelm |
tuned: more antiquotations;
|
changeset |
files
|
| Thu, 08 Aug 2024 14:24:18 +0200 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Thu, 08 Aug 2024 18:56:14 +0100 |
paulson |
Two little lemmas
|
changeset |
files
|
| Wed, 07 Aug 2024 20:56:31 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 07 Aug 2024 20:15:03 +0200 |
wenzelm |
more uniform Type_Infer_Context.infer_types_finished, despite subtle differences of Type_Infer.fixate vs. Proof_Context.standard_term_check_finish;
|
changeset |
files
|
| Wed, 07 Aug 2024 20:11:05 +0200 |
wenzelm |
tuned, following cdae621613da;
|
changeset |
files
|
| Wed, 07 Aug 2024 20:07:50 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 07 Aug 2024 20:06:55 +0200 |
wenzelm |
more robust: only type inference with its finish/fixate phase (on contrast to dc387e3999ec), e.g. avoid accidental "improvement" of type class operations (free vs. const);
|
changeset |
files
|
| Wed, 07 Aug 2024 16:28:32 +0200 |
wenzelm |
tuned: more antiquotations;
|
changeset |
files
|
| Wed, 07 Aug 2024 16:26:54 +0200 |
wenzelm |
tuned: more abstract access to datatype typ;
|
changeset |
files
|
| Wed, 07 Aug 2024 15:37:27 +0200 |
wenzelm |
tuned (see also db120661dded);
|
changeset |
files
|
| Wed, 07 Aug 2024 15:11:54 +0200 |
wenzelm |
tuned: more antiquotations;
|
changeset |
files
|
| Wed, 07 Aug 2024 14:44:51 +0200 |
wenzelm |
tuned signature: eliminate aliases;
|
changeset |
files
|
| Wed, 07 Aug 2024 13:54:09 +0200 |
wenzelm |
removed odd clone (amending 100c0eaf63d5);
|
changeset |
files
|
| Wed, 07 Aug 2024 13:45:37 +0200 |
wenzelm |
clarified: more robust (dest_Type_name o body_type), which may fail in both parts;
|
changeset |
files
|
| Wed, 07 Aug 2024 13:25:51 +0200 |
wenzelm |
tuned: more antiquotations, more abstract access to datatype typ;
|
changeset |
files
|
| Wed, 07 Aug 2024 12:50:22 +0200 |
wenzelm |
recover lost update (see 11b8f2e4c3d2 and 4041e7c8059d);
|
changeset |
files
|
| Wed, 07 Aug 2024 11:58:45 +0200 |
wenzelm |
prefer host that is less likely to be down;
|
changeset |
files
|
| Wed, 07 Aug 2024 11:58:01 +0200 |
wenzelm |
tuned: more antiquotations, avoid re-certification;
|
changeset |
files
|
| Wed, 07 Aug 2024 12:39:09 +0100 |
paulson |
Rearranged a couple of theorems
|
changeset |
files
|
| Tue, 06 Aug 2024 22:47:44 +0100 |
paulson |
New library material; also fixed the spelling error powr_ge_pzero -> powr_ge_zero
|
changeset |
files
|
| Tue, 06 Aug 2024 18:14:45 +0100 |
paulson |
merged
|
changeset |
files
|
| Wed, 31 Jul 2024 18:47:05 +0100 |
paulson |
tidied more apply proofs
|
changeset |
files
|
| Tue, 06 Aug 2024 18:39:32 +0200 |
Fabian Huch |
build_manager: change colors;
|
changeset |
files
|
| Tue, 06 Aug 2024 16:58:23 +0200 |
Fabian Huch |
build_manager: display more info;
|
changeset |
files
|
| Tue, 06 Aug 2024 16:58:05 +0200 |
Fabian Huch |
add tables to web_app;
|
changeset |
files
|
| Tue, 06 Aug 2024 15:40:51 +0200 |
Fabian Huch |
tuned and clarified;
|
changeset |
files
|
| Tue, 06 Aug 2024 15:38:10 +0200 |
Fabian Huch |
build_manager: store submitting user;
|
changeset |
files
|
| Tue, 06 Aug 2024 15:00:37 +0200 |
Fabian Huch |
build_manager: terminate processes if cancelling does not work;
|
changeset |
files
|
| Tue, 06 Aug 2024 13:54:10 +0200 |
Fabian Huch |
build_manager: log message when job is cancelled;
|
changeset |
files
|
| Tue, 06 Aug 2024 12:31:42 +0200 |
nipkow |
branches of case expressions may need to be eta-expanded
|
changeset |
files
|
| Mon, 05 Aug 2024 20:30:50 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 05 Aug 2024 19:57:23 +0200 |
wenzelm |
tuned: more antiquotations;
|
changeset |
files
|
| Sun, 04 Aug 2024 23:50:44 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 04 Aug 2024 23:17:35 +0200 |
wenzelm |
tuned: more standard Isabelle/ML;
|
changeset |
files
|
| Sun, 04 Aug 2024 22:59:51 +0200 |
wenzelm |
clarified signature: prefer local context;
|
changeset |
files
|
| Sun, 04 Aug 2024 22:45:20 +0200 |
wenzelm |
tuned: more antiquotations;
|
changeset |
files
|
| Sun, 04 Aug 2024 17:39:47 +0200 |
wenzelm |
tuned: more explicit dest_Const_name and dest_Const_type;
|
changeset |
files
|
| Sun, 04 Aug 2024 16:56:28 +0200 |
wenzelm |
tuned signature: more operations;
|
changeset |
files
|
| Sun, 04 Aug 2024 13:24:54 +0200 |
wenzelm |
tuned: more explicit dest_Type_name and dest_Type_args;
|
changeset |
files
|
| Sun, 04 Aug 2024 13:14:33 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 04 Aug 2024 12:21:13 +0200 |
wenzelm |
tuned signature: more operations;
|
changeset |
files
|
| Sat, 03 Aug 2024 13:12:58 +0200 |
wenzelm |
tuned: more antiquotations;
|
changeset |
files
|
| Fri, 02 Aug 2024 18:25:18 +0200 |
nipkow |
got rid of references to system-generated names
|
changeset |
files
|
| Thu, 01 Aug 2024 14:07:34 +0200 |
nipkow |
tuned names
|
changeset |
files
|
| Wed, 31 Jul 2024 10:36:28 +0200 |
nipkow |
tuned names
|
changeset |
files
|
| Mon, 29 Jul 2024 16:22:12 +0100 |
paulson |
merged
|
changeset |
files
|
| Mon, 29 Jul 2024 16:22:05 +0100 |
paulson |
Reversed my brain-dead stupid change to divide_left_mono and divide_left_mono_neg
|
changeset |
files
|
| Mon, 29 Jul 2024 15:26:56 +0200 |
nipkow |
merged
|
changeset |
files
|
| Mon, 29 Jul 2024 15:26:03 +0200 |
nipkow |
time_function T_map can now be generated automatically.
|
changeset |
files
|
| Mon, 29 Jul 2024 10:49:17 +0100 |
paulson |
Further divide_mono fixes
|
changeset |
files
|
| Mon, 29 Jul 2024 10:24:54 +0100 |
paulson |
Fix for simplified divide_mono theorem
|
changeset |
files
|
| Mon, 29 Jul 2024 10:13:52 +0100 |
paulson |
Migration of new material mostly about exp, ln
|
changeset |
files
|
| Sun, 28 Jul 2024 14:45:41 +0100 |
paulson |
More simplification of a nominal example
|
changeset |
files
|
| Sat, 27 Jul 2024 11:41:17 +0100 |
paulson |
merged
|
changeset |
files
|
| Sat, 27 Jul 2024 11:41:08 +0100 |
paulson |
More simplification of apply proofs
|
changeset |
files
|
| Fri, 26 Jul 2024 22:32:31 +0200 |
wenzelm |
less ambitious parallelism: avoid exhaustion of memory (64GB total);
|
changeset |
files
|
| Thu, 25 Jul 2024 10:30:22 +0200 |
wenzelm |
tuned names;
|
changeset |
files
|
| Wed, 24 Jul 2024 19:08:08 +0100 |
paulson |
merged
|
changeset |
files
|
| Wed, 24 Jul 2024 19:07:59 +0100 |
paulson |
Adjusting the precedences to reduce syntactic ambiguity
|
changeset |
files
|
| Tue, 23 Jul 2024 22:50:59 +0200 |
wenzelm |
disable thy_cache for now (amending 0b8922e351a3): avoid crash of AFP/Ramsey-Infinite due to exception THEORY "Duplicate theory name";
|
changeset |
files
|
| Tue, 23 Jul 2024 15:54:43 +0100 |
paulson |
A lot of new material from the Ramsey development, including a couple of new simprules.
|
changeset |
files
|
| Mon, 22 Jul 2024 22:55:19 +0100 |
paulson |
A massive reduction of some truly horrible proofs
|
changeset |
files
|
| Mon, 22 Jul 2024 20:13:46 +0100 |
paulson |
merged
|
changeset |
files
|
| Mon, 22 Jul 2024 20:13:38 +0100 |
paulson |
More simplification of proofs. Trying to fix the syntax too
|
changeset |
files
|
| Sun, 21 Jul 2024 23:31:32 +0200 |
wenzelm |
clarified export: replaced Proofterm.standard_vars by ZTerm.standard_vars;
|
changeset |
files
|
| Sun, 21 Jul 2024 22:34:25 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 21 Jul 2024 22:01:03 +0200 |
wenzelm |
clarified order of operations: no_thm_names first;
|
changeset |
files
|
| Sun, 21 Jul 2024 20:00:13 +0200 |
wenzelm |
more operations;
|
changeset |
files
|
| Sun, 21 Jul 2024 13:44:05 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 21 Jul 2024 13:04:01 +0200 |
wenzelm |
more operations;
|
changeset |
files
|
| Sun, 21 Jul 2024 13:03:33 +0200 |
wenzelm |
more operations;
|
changeset |
files
|
| Sun, 21 Jul 2024 12:37:37 +0200 |
wenzelm |
clarified signature: more robust operations;
|
changeset |
files
|
| Sat, 20 Jul 2024 22:43:27 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Sat, 20 Jul 2024 21:17:22 +0200 |
wenzelm |
clarified modules (see also e063c0403650);
|
changeset |
files
|
| Sat, 20 Jul 2024 19:30:03 +0200 |
wenzelm |
more operations;
|
changeset |
files
|
| Sat, 20 Jul 2024 16:34:16 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 20 Jul 2024 12:35:43 +0200 |
wenzelm |
tuned: more direct Name.context for bounds;
|
changeset |
files
|
| Sat, 20 Jul 2024 16:47:04 +0100 |
paulson |
Got rid of another 250 apply-lines
|
changeset |
files
|
| Fri, 19 Jul 2024 22:29:32 +0100 |
paulson |
merged
|
changeset |
files
|
| Fri, 19 Jul 2024 22:29:16 +0100 |
paulson |
more proof tidying
|
changeset |
files
|
| Fri, 19 Jul 2024 19:57:20 +0200 |
wenzelm |
more predictable proof id;
|
changeset |
files
|
| Fri, 19 Jul 2024 17:58:13 +0200 |
wenzelm |
more conservative cache: retain concurrent value;
|
changeset |
files
|
| Fri, 19 Jul 2024 16:58:52 +0200 |
wenzelm |
clarified thm_header command_pos vs. thm_pos;
|
changeset |
files
|
| Fri, 19 Jul 2024 11:29:05 +0200 |
wenzelm |
clarified signature, following zterm.ML;
|
changeset |
files
|
| Fri, 19 Jul 2024 11:28:25 +0200 |
wenzelm |
tuned whitespace;
|
changeset |
files
|
| Thu, 18 Jul 2024 17:02:39 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Thu, 18 Jul 2024 16:25:53 +0200 |
wenzelm |
uniform export via ztyp/zterm/zproof;
|
changeset |
files
|
| Thu, 18 Jul 2024 15:26:36 +0200 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Thu, 18 Jul 2024 12:08:08 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 18 Jul 2024 11:36:09 +0200 |
wenzelm |
more operations;
|
changeset |
files
|
| Thu, 18 Jul 2024 11:02:08 +0200 |
wenzelm |
clarified scope of cache: avoid nested typ_cache;
|
changeset |
files
|
| Thu, 18 Jul 2024 10:45:36 +0200 |
wenzelm |
clarified scope of cache: per theory body;
|
changeset |
files
|
| Tue, 16 Jul 2024 12:49:23 +0200 |
wenzelm |
tuned module structure;
|
changeset |
files
|
| Mon, 15 Jul 2024 12:26:15 +0200 |
wenzelm |
clarified signature: more operations;
|
changeset |
files
|
| Thu, 18 Jul 2024 16:00:40 +0200 |
nipkow |
merged
|
changeset |
files
|
| Thu, 18 Jul 2024 15:57:07 +0200 |
nipkow |
tuned
|
changeset |
files
|
| Thu, 18 Jul 2024 15:17:46 +0200 |
nipkow |
added nicer proof
|
changeset |
files
|
| Thu, 18 Jul 2024 13:52:51 +0200 |
Fabian Huch |
better poller: don't start job when same version is already running;
|
changeset |
files
|
| Thu, 18 Jul 2024 13:08:11 +0200 |
Fabian Huch |
clarified: more uniform;
|
changeset |
files
|
| Thu, 18 Jul 2024 10:43:55 +0200 |
desharna |
merged
|
changeset |
files
|
| Wed, 17 Jul 2024 17:48:23 +0200 |
desharna |
added lemmas wfp_on_antimono_stronger and wf_on_antimono_stronger
|
changeset |
files
|
| Wed, 17 Jul 2024 21:25:37 +0100 |
paulson |
More streamlining
|
changeset |
files
|
| Mon, 15 Jul 2024 21:48:30 +0100 |
paulson |
merged
|
changeset |
files
|
| Mon, 15 Jul 2024 21:48:23 +0100 |
paulson |
Revised mixfix and streamlined proofs
|
changeset |
files
|
| Sun, 14 Jul 2024 18:10:06 +0200 |
wenzelm |
clarified Isabelle/Haskell type Term, following Isabelle/Scala (see 446b887e23c7);
|
changeset |
files
|
| Sun, 14 Jul 2024 17:56:54 +0200 |
wenzelm |
tuned output, following Isabelle/Scala;
|
changeset |
files
|
| Sun, 14 Jul 2024 17:49:30 +0200 |
wenzelm |
clarified data representation: prefer explicit OFCLASS constructor, following datatype zterm;
|
changeset |
files
|
| Sun, 14 Jul 2024 16:17:31 +0200 |
wenzelm |
clarified signature, following Isabelle/Scala;
|
changeset |
files
|
| Sun, 14 Jul 2024 16:07:03 +0200 |
wenzelm |
afford larger example (see also ccf9241af217);
|
changeset |
files
|
| Sun, 14 Jul 2024 15:56:58 +0200 |
wenzelm |
more scalable operations;
|
changeset |
files
|
| Sun, 14 Jul 2024 15:50:42 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 14 Jul 2024 15:49:26 +0200 |
wenzelm |
tuned (see also 4879d0021185);
|
changeset |
files
|
| Sun, 14 Jul 2024 15:16:08 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Fri, 12 Jul 2024 14:18:56 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Thu, 11 Jul 2024 23:36:54 +0200 |
wenzelm |
clarified signature: afford explicit Scala data types;
|
changeset |
files
|
| Thu, 11 Jul 2024 22:39:04 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Thu, 11 Jul 2024 22:29:54 +0200 |
wenzelm |
tuned signature (again);
|
changeset |
files
|
| Thu, 11 Jul 2024 18:25:25 +0200 |
wenzelm |
clarified signature: more self-contained paint_chunk_list;
|
changeset |
files
|
| Thu, 11 Jul 2024 15:51:19 +0200 |
wenzelm |
clarified signature: more arguments;
|
changeset |
files
|
| Thu, 11 Jul 2024 13:33:58 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 11 Jul 2024 11:39:36 +0200 |
wenzelm |
clarified popup layer (not relevant yet);
|
changeset |
files
|
| Thu, 11 Jul 2024 11:13:21 +0200 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Tue, 09 Jul 2024 13:16:57 +0200 |
wenzelm |
misc tuning and clarification;
|
changeset |
files
|
| Tue, 09 Jul 2024 12:41:05 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 09 Jul 2024 12:32:33 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Wed, 10 Jul 2024 17:42:48 +0200 |
Fabian Huch |
tuned website;
|
changeset |
files
|
| Wed, 10 Jul 2024 17:31:17 +0200 |
Fabian Huch |
proper parse (amending dd86d35375a7);
|
changeset |
files
|
| Wed, 10 Jul 2024 17:04:44 +0200 |
Fabian Huch |
allow updating reports via build_manager_database tool, e.g. to generate hg logs/diffs;
|
changeset |
files
|
| Wed, 10 Jul 2024 17:01:51 +0200 |
Fabian Huch |
clarified;
|
changeset |
files
|
| Wed, 10 Jul 2024 16:58:39 +0200 |
Fabian Huch |
clarified;
|
changeset |
files
|
| Wed, 10 Jul 2024 16:56:59 +0200 |
Fabian Huch |
log and display components with empty (unknown) revisions to indicate that they are present;
|
changeset |
files
|
| Wed, 10 Jul 2024 09:58:32 +0200 |
Fabian Huch |
tuned log: omit previous changeset;
|
changeset |
files
|
| Wed, 10 Jul 2024 08:37:54 +0200 |
nipkow |
take care of facts in cartouches
|
changeset |
files
|
| Tue, 09 Jul 2024 21:13:14 +0100 |
paulson |
Simplified a few proofs
|
changeset |
files
|
| Tue, 09 Jul 2024 16:06:32 +0200 |
Fabian Huch |
tuned display;
|
changeset |
files
|
| Tue, 09 Jul 2024 16:00:25 +0200 |
Fabian Huch |
NEWS and CONTRIBUTORS;
|
changeset |
files
|
| Tue, 09 Jul 2024 15:06:24 +0200 |
Fabian Huch |
tuned HTML display of ANSI colors for better readability;
|
changeset |
files
|
| Tue, 09 Jul 2024 14:13:59 +0200 |
Fabian Huch |
render hg diff and log (on separate page);
|
changeset |
files
|
| Tue, 09 Jul 2024 13:58:43 +0200 |
Fabian Huch |
clarified;
|
changeset |
files
|
| Tue, 09 Jul 2024 12:56:27 +0200 |
Fabian Huch |
store hg log in addition to diff;
|
changeset |
files
|
| Tue, 09 Jul 2024 11:20:09 +0200 |
Fabian Huch |
clarified names;
|
changeset |
files
|
| Tue, 09 Jul 2024 11:11:15 +0200 |
Fabian Huch |
tuned;
|
changeset |
files
|
| Tue, 09 Jul 2024 11:23:50 +0100 |
paulson |
NEWS: totalisation of ln
|
changeset |
files
|
| Mon, 08 Jul 2024 22:28:02 +0100 |
paulson |
merged
|
changeset |
files
|
| Mon, 08 Jul 2024 22:27:50 +0100 |
paulson |
Better multiplication and division rules for ln and log
|
changeset |
files
|
| Mon, 08 Jul 2024 17:57:19 +0200 |
wenzelm |
ignore error code for "isabelle worker" (in contrast to eff08c3f89fe): avoid confusing "failed to work" messages via Build_Cluster.start;
|
changeset |
files
|
| Mon, 08 Jul 2024 17:44:20 +0200 |
wenzelm |
disable old tests;
|
changeset |
files
|
| Mon, 08 Jul 2024 10:14:22 +0200 |
desharna |
added lemma image_mset_diff_if_inj
|
changeset |
files
|
| Mon, 08 Jul 2024 10:08:07 +0200 |
desharna |
added lemma minus_add_mset_if_not_in_lhs[simp]
|
changeset |
files
|
| Sun, 07 Jul 2024 22:25:34 +0100 |
paulson |
last-minute correction: no simprule for ln_minus
|
changeset |
files
|
| Sat, 06 Jul 2024 12:51:43 +0100 |
paulson |
merged
|
changeset |
files
|
| Sat, 06 Jul 2024 12:51:31 +0100 |
paulson |
Totalisation of ln and therefore log and powr
|
changeset |
files
|
| Fri, 05 Jul 2024 21:59:43 +0100 |
paulson |
merged
|
changeset |
files
|
| Fri, 05 Jul 2024 21:58:40 +0100 |
paulson |
The changes needed to reduce the need to snoop on edits to theory files
|
changeset |
files
|
| Sat, 06 Jul 2024 11:18:31 +0200 |
wenzelm |
tuned messages: whitespace following usual Isabelle conventions;
|
changeset |
files
|
| Fri, 05 Jul 2024 16:34:17 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Fri, 05 Jul 2024 16:28:05 +0200 |
wenzelm |
reactivate mini2 long after upgrade (see also a11c461a1a3a);
|
changeset |
files
|
| Fri, 05 Jul 2024 14:01:14 +0200 |
wenzelm |
NEWS;
|
changeset |
files
|
| Fri, 05 Jul 2024 13:46:13 +0200 |
wenzelm |
tuned signature: expose internal limits for testing or add-on implementations;
|
changeset |
files
|
| Fri, 05 Jul 2024 13:41:01 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 05 Jul 2024 13:38:35 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 05 Jul 2024 13:36:49 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 05 Jul 2024 13:04:39 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 05 Jul 2024 12:53:45 +0200 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Fri, 05 Jul 2024 11:38:21 +0200 |
wenzelm |
prefer official UTF-8 decoding (in contrast to 2541de190d92): this is also more efficient (factor 10-20);
|
changeset |
files
|
| Fri, 05 Jul 2024 10:55:02 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 05 Jul 2024 00:21:47 +0200 |
wenzelm |
unused (see also c2f176a38448);
|
changeset |
files
|
| Fri, 05 Jul 2024 00:18:51 +0200 |
wenzelm |
more robust message header: prefer explicit props_length/props_chunks over odd YXML.embed_controls;
|
changeset |
files
|
| Fri, 05 Jul 2024 00:12:32 +0200 |
wenzelm |
tuned signature: more operations;
|
changeset |
files
|
| Thu, 04 Jul 2024 19:16:12 +0200 |
wenzelm |
tuned comments;
|
changeset |
files
|
| Fri, 05 Jul 2024 10:38:17 +0200 |
Fabian Huch |
tuned whitespace;
|
changeset |
files
|
| Fri, 05 Jul 2024 09:52:56 +0200 |
Fabian Huch |
use ansi colored diffs;
|
changeset |
files
|
| Fri, 05 Jul 2024 09:47:21 +0200 |
Fabian Huch |
add diffs to build manager;
|
changeset |
files
|
| Thu, 04 Jul 2024 13:50:14 +0200 |
Fabian Huch |
clarified: components vs. extra components;
|
changeset |
files
|
| Thu, 04 Jul 2024 09:57:40 +0200 |
Fabian Huch |
compress reports;
|
changeset |
files
|
| Wed, 03 Jul 2024 21:11:24 +0200 |
Fabian Huch |
clarified build report;
|
changeset |
files
|
| Wed, 03 Jul 2024 21:54:17 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 03 Jul 2024 21:22:52 +0200 |
wenzelm |
enforce rebuild of Isabelle/ML;
|
changeset |
files
|
| Wed, 03 Jul 2024 21:11:53 +0200 |
wenzelm |
clarified signature, following 43323d886ea3;
|
changeset |
files
|
| Wed, 03 Jul 2024 20:59:30 +0200 |
wenzelm |
clarified signature: more direct operation;
|
changeset |
files
|
| Wed, 03 Jul 2024 20:35:10 +0200 |
wenzelm |
clarified signature: more direct Bytes.raw and subsequent UTF-8 default decoding;
|
changeset |
files
|
| Wed, 03 Jul 2024 20:18:36 +0200 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Wed, 03 Jul 2024 15:24:34 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 03 Jul 2024 13:54:48 +0200 |
wenzelm |
unused;
|
changeset |
files
|
| Wed, 03 Jul 2024 10:16:39 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 03 Jul 2024 10:14:47 +0200 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Wed, 03 Jul 2024 10:09:59 +0200 |
wenzelm |
unused;
|
changeset |
files
|
| Wed, 03 Jul 2024 10:07:39 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Wed, 03 Jul 2024 19:42:13 +0200 |
nipkow |
simpler theorem
|
changeset |
files
|
| Wed, 03 Jul 2024 09:14:39 +0200 |
Fabian Huch |
clarified: control verbosity;
|
changeset |
files
|
| Tue, 02 Jul 2024 23:29:46 +0200 |
wenzelm |
enforce rebuild of Isabelle/ML;
|
changeset |
files
|
| Tue, 02 Jul 2024 23:28:55 +0200 |
wenzelm |
more uniform Bytes.read_stream vs. File.read_stream;
|
changeset |
files
|
| Tue, 02 Jul 2024 23:13:35 +0200 |
wenzelm |
clarified YXML.Source: more direct support for String and Bytes, instead of CharSequence;
|
changeset |
files
|
| Tue, 02 Jul 2024 22:38:00 +0200 |
wenzelm |
more specialized operations;
|
changeset |
files
|
| Tue, 02 Jul 2024 21:54:12 +0200 |
wenzelm |
notable performance tuning for Library.separated_chunks variants;
|
changeset |
files
|
| Tue, 02 Jul 2024 21:35:40 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 02 Jul 2024 17:38:28 +0200 |
Fabian Huch |
only consider jobs late if they have ancestors (amending 12901c03b416);
|
changeset |
files
|
| Tue, 02 Jul 2024 16:42:13 +0200 |
wenzelm |
enforce rebuild of Isabelle/ML;
|
changeset |
files
|
| Tue, 02 Jul 2024 16:36:49 +0200 |
wenzelm |
misc tuning: more uniform read_stream vs. read_file;
|
changeset |
files
|
| Tue, 02 Jul 2024 16:15:50 +0200 |
wenzelm |
proper limit for read operation (amending ac4d53bc8f6b);
|
changeset |
files
|
| Tue, 02 Jul 2024 15:30:59 +0200 |
wenzelm |
presumably unused (see also f992769dea97);
|
changeset |
files
|
| Mon, 01 Jul 2024 18:22:33 +0200 |
Fabian Huch |
remove inactive (e.g., crashed) hosts from scheduling;
|
changeset |
files
|
| Mon, 01 Jul 2024 15:25:27 +0200 |
Fabian Huch |
tuned;
|
changeset |
files
|
| Mon, 01 Jul 2024 15:24:04 +0200 |
Fabian Huch |
add timeout to build manager tasks/jobs (e.g. for cluster builds that don't terminate after error on host);
|
changeset |
files
|
| Mon, 01 Jul 2024 14:46:51 +0200 |
Fabian Huch |
clarified: more operations;
|
changeset |
files
|
| Mon, 01 Jul 2024 14:31:30 +0200 |
Fabian Huch |
tuned website;
|
changeset |
files
|
| Mon, 01 Jul 2024 13:11:25 +0200 |
wenzelm |
more significant HOL/Examples;
|
changeset |
files
|
| Mon, 01 Jul 2024 13:09:03 +0200 |
wenzelm |
tuned document layout, for more prominent presentation;
|
changeset |
files
|
| Mon, 01 Jul 2024 12:59:46 +0200 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Mon, 01 Jul 2024 12:59:18 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 01 Jul 2024 12:40:54 +0200 |
wenzelm |
clarified signature: more explicit XML.Body types, more uniform Symbol.encode_yxml;
|
changeset |
files
|
| Mon, 01 Jul 2024 12:37:03 +0200 |
wenzelm |
tuned signature: more operations;
|
changeset |
files
|
| Sun, 30 Jun 2024 13:20:54 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Sun, 30 Jun 2024 13:20:40 +0200 |
wenzelm |
follow Phorge 2024 week 19;
|
changeset |
files
|
| Sun, 30 Jun 2024 11:13:31 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Sat, 29 Jun 2024 14:57:04 +0200 |
wenzelm |
minor performance tuning;
|
changeset |
files
|
| Sat, 29 Jun 2024 14:48:20 +0200 |
wenzelm |
clarified modules;
|
changeset |
files
|
| Sat, 29 Jun 2024 12:50:43 +0200 |
wenzelm |
minor performance tuning;
|
changeset |
files
|
| Sat, 29 Jun 2024 12:42:47 +0200 |
wenzelm |
minor performance tuning;
|
changeset |
files
|
| Sun, 30 Jun 2024 06:30:08 +0000 |
haftmann |
moved transitional theory Divides to HOL-Library
|
changeset |
files
|
| Thu, 27 Jun 2024 16:52:17 +0000 |
haftmann |
dropped dubious dest rule which always unfolds a definition in the assumptions
|
changeset |
files
|
| Fri, 28 Jun 2024 23:53:48 +0200 |
wenzelm |
more robust: avoid indirection of repository servers;
|
changeset |
files
|
| Fri, 28 Jun 2024 23:53:25 +0200 |
wenzelm |
tuned output;
|
changeset |
files
|
| Fri, 28 Jun 2024 21:01:57 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Fri, 28 Jun 2024 18:30:26 +0200 |
wenzelm |
enforce rebuild of Isabelle/ML;
|
changeset |
files
|
| Fri, 28 Jun 2024 16:51:55 +0200 |
wenzelm |
minor performance tuning: allow recode operation during YXML parsing;
|
changeset |
files
|
| Fri, 28 Jun 2024 15:59:45 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 28 Jun 2024 13:25:51 +0200 |
wenzelm |
minor performance tuning;
|
changeset |
files
|
| Fri, 28 Jun 2024 13:46:06 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 28 Jun 2024 13:20:18 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 28 Jun 2024 13:14:15 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 28 Jun 2024 11:37:13 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 28 Jun 2024 11:09:58 +0200 |
wenzelm |
tuned signature, following Bytes.Builder.use;
|
changeset |
files
|
| Fri, 28 Jun 2024 00:30:49 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Fri, 28 Jun 2024 00:26:02 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 28 Jun 2024 00:15:34 +0200 |
wenzelm |
minor performance tuning: more direct Bytes with Symbol.encode;
|
changeset |
files
|
| Thu, 27 Jun 2024 23:53:31 +0200 |
wenzelm |
minor performance tuning: more direct YXML.bytes_of_body;
|
changeset |
files
|
| Thu, 27 Jun 2024 23:45:32 +0200 |
wenzelm |
more robust: prefer tail-recursive traversal;
|
changeset |
files
|
| Thu, 27 Jun 2024 23:36:19 +0200 |
wenzelm |
tuned module structure;
|
changeset |
files
|
| Thu, 27 Jun 2024 23:32:24 +0200 |
wenzelm |
more robust: prefer tail-recursive XML.Traversal;
|
changeset |
files
|
| Thu, 27 Jun 2024 23:27:41 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 27 Jun 2024 23:18:28 +0200 |
wenzelm |
clarified treatment of empty markup;
|
changeset |
files
|
| Thu, 27 Jun 2024 22:39:20 +0200 |
wenzelm |
more robust: prefer tail-recursive traversal;
|
changeset |
files
|
| Thu, 27 Jun 2024 22:09:09 +0200 |
wenzelm |
clarified signature: more explicit types;
|
changeset |
files
|
| Thu, 27 Jun 2024 00:11:53 +0200 |
wenzelm |
minor performance tuning;
|
changeset |
files
|
| Thu, 27 Jun 2024 00:09:37 +0200 |
wenzelm |
more operations;
|
changeset |
files
|
| Thu, 27 Jun 2024 00:01:01 +0200 |
wenzelm |
performance tuning: multi-stage buffer with fewer array copies;
|
changeset |
files
|
| Wed, 26 Jun 2024 15:22:20 +0200 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Fri, 28 Jun 2024 17:13:25 +0200 |
Fabian Huch |
abort tasks with invalid host specs;
|
changeset |
files
|
| Fri, 28 Jun 2024 16:18:40 +0200 |
Fabian Huch |
tuned cli;
|
changeset |
files
|
| Fri, 28 Jun 2024 13:49:29 +0200 |
Fabian Huch |
proper build command;
|
changeset |
files
|
| Fri, 28 Jun 2024 12:10:26 +0200 |
Fabian Huch |
tuned website;
|
changeset |
files
|
| Fri, 28 Jun 2024 11:51:46 +0200 |
Fabian Huch |
better results view;
|
changeset |
files
|
| Fri, 28 Jun 2024 11:33:09 +0200 |
Fabian Huch |
better build summaries;
|
changeset |
files
|
| Fri, 28 Jun 2024 11:09:04 +0200 |
Fabian Huch |
add timing messages;
|
changeset |
files
|
| Fri, 28 Jun 2024 10:58:29 +0200 |
Fabian Huch |
clarified: use progress start date;
|
changeset |
files
|
| Fri, 28 Jun 2024 09:54:06 +0200 |
Fabian Huch |
clarified: more operations;
|
changeset |
files
|
| Thu, 27 Jun 2024 11:59:12 +0200 |
Fabian Huch |
tuned comment;
|
changeset |
files
|
| Thu, 27 Jun 2024 09:41:16 +0200 |
Fabian Huch |
add Isabelle settings to managed tasks and ci jobs;
|
changeset |
files
|
| Wed, 26 Jun 2024 19:55:56 +0200 |
Fabian Huch |
remove unused Jenkins component;
|
changeset |
files
|
| Wed, 12 Jun 2024 17:12:13 +0200 |
Fabian Huch |
moved ci_build module to build_ci;
|
changeset |
files
|
| Wed, 12 Jun 2024 17:06:34 +0200 |
Fabian Huch |
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
|
changeset |
files
|
| Tue, 25 Jun 2024 18:09:53 +0200 |
Fabian Huch |
tuned;
|
changeset |
files
|
| Tue, 25 Jun 2024 17:57:08 +0200 |
Fabian Huch |
tuned;
|
changeset |
files
|
| Tue, 25 Jun 2024 17:56:49 +0200 |
Fabian Huch |
add root entry for non-local components;
|
changeset |
files
|
| Tue, 25 Jun 2024 17:55:37 +0200 |
Fabian Huch |
clarified;
|
changeset |
files
|
| Tue, 25 Jun 2024 13:53:45 +0200 |
Fabian Huch |
extra timer delay, to limit db transactions;
|
changeset |
files
|
| Tue, 25 Jun 2024 13:44:20 +0200 |
Fabian Huch |
proper synchronized;
|
changeset |
files
|
| Tue, 25 Jun 2024 11:08:00 +0200 |
nipkow |
clarified ternary tries
|
changeset |
files
|
| Mon, 24 Jun 2024 22:52:54 +0200 |
wenzelm |
clarified test parameters;
|
changeset |
files
|
| Sat, 22 Jun 2024 22:07:41 +0200 |
wenzelm |
more tests: Windows + AFP (see also 1fd5f96e1da3);
|
changeset |
files
|
| Thu, 20 Jun 2024 14:28:46 +0000 |
haftmann |
dropped references to theorems from transitional theory Divides.thy
|
changeset |
files
|
| Wed, 19 Jun 2024 12:13:16 +0200 |
paulson |
Tidied some messy proofs
|
changeset |
files
|
| Wed, 19 Jun 2024 10:20:35 +0200 |
paulson |
Updated some archaic proofs
|
changeset |
files
|
| Tue, 18 Jun 2024 16:55:30 +0200 |
nipkow |
tuned def: patter matching needs more beautification
|
changeset |
files
|
| Mon, 17 Jun 2024 09:00:46 +0200 |
desharna |
removed lemma wellorder.wfP_less
|
changeset |
files
|
| Sun, 16 Jun 2024 21:54:09 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Sun, 16 Jun 2024 21:53:24 +0200 |
wenzelm |
enforce rebuild of Isabelle/ML;
|
changeset |
files
|
| Sun, 16 Jun 2024 18:50:17 +0200 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Sun, 16 Jun 2024 18:41:57 +0200 |
wenzelm |
Base64: proper support for large Bytes, with subtle change of types (Bytes instead of String);
|
changeset |
files
|
| Sun, 16 Jun 2024 18:18:55 +0200 |
wenzelm |
tuned: prefer Bytes operations;
|
changeset |
files
|
| Sun, 16 Jun 2024 18:17:54 +0200 |
wenzelm |
unused;
|
changeset |
files
|
| Sun, 16 Jun 2024 17:37:52 +0200 |
wenzelm |
proper treatment of long message blocks;
|
changeset |
files
|
| Sun, 16 Jun 2024 14:21:57 +0200 |
wenzelm |
clarified sizes;
|
changeset |
files
|
| Sun, 16 Jun 2024 14:19:51 +0200 |
wenzelm |
more scalable stream read operations;
|
changeset |
files
|
| Sun, 16 Jun 2024 11:59:16 +0200 |
wenzelm |
minor performance tuning;
|
changeset |
files
|
| Sun, 16 Jun 2024 11:55:25 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 16 Jun 2024 11:50:42 +0200 |
wenzelm |
tuned module structure;
|
changeset |
files
|
| Sun, 16 Jun 2024 11:41:22 +0200 |
wenzelm |
tuned names;
|
changeset |
files
|
| Sun, 16 Jun 2024 11:28:47 +0200 |
wenzelm |
imitate internal policy of ByteArrayOutputStream: capacity is doubled after first push;
|
changeset |
files
|
| Sat, 15 Jun 2024 23:52:30 +0200 |
wenzelm |
tuned whitespace;
|
changeset |
files
|
| Sat, 15 Jun 2024 23:49:06 +0200 |
wenzelm |
unused;
|
changeset |
files
|
| Sat, 15 Jun 2024 23:47:04 +0200 |
wenzelm |
Bytes.Builder is unsynchronized, like java.io.OutputBuffer;
|
changeset |
files
|
| Sat, 15 Jun 2024 23:24:24 +0200 |
wenzelm |
notable performance tuning: avoid overhead of higher-order functions;
|
changeset |
files
|
| Sat, 15 Jun 2024 22:43:01 +0200 |
wenzelm |
more efficient equals: avoid somewhat slow sha1_digest (see also 29b761e290c5, 306f273c91ec);
|
changeset |
files
|
| Sat, 15 Jun 2024 21:59:31 +0200 |
wenzelm |
more scalable compression, using Bytes.Builder.Stream;
|
changeset |
files
|
| Sat, 15 Jun 2024 21:52:14 +0200 |
wenzelm |
tuned: more uniform, less ambitious;
|
changeset |
files
|
| Sat, 15 Jun 2024 21:07:23 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 15 Jun 2024 20:49:15 +0200 |
wenzelm |
minor performance tuning;
|
changeset |
files
|
| Sat, 15 Jun 2024 20:44:09 +0200 |
wenzelm |
minor performance tuning;
|
changeset |
files
|
| Sat, 15 Jun 2024 20:30:31 +0200 |
wenzelm |
minor performance tuning;
|
changeset |
files
|
| Sat, 15 Jun 2024 20:29:50 +0200 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Sat, 15 Jun 2024 20:17:43 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 15 Jun 2024 20:14:53 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 15 Jun 2024 20:14:24 +0200 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Sat, 15 Jun 2024 17:16:14 +0200 |
wenzelm |
minor performance tuning;
|
changeset |
files
|
| Sat, 15 Jun 2024 17:12:49 +0200 |
wenzelm |
support large byte arrays, using multiple "chunks";
|
changeset |
files
|
| Sat, 15 Jun 2024 12:27:57 +0200 |
wenzelm |
clarified File.eq_content, following 306f273c91ec;
|
changeset |
files
|
| Thu, 13 Jun 2024 15:08:24 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 12 Jun 2024 22:09:16 +0200 |
wenzelm |
clarified hash and equality: depend on sha1 digest to be collision-free;
|
changeset |
files
|
| Wed, 12 Jun 2024 21:59:44 +0200 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Wed, 12 Jun 2024 21:56:01 +0200 |
wenzelm |
tuned source structure;
|
changeset |
files
|
| Wed, 12 Jun 2024 21:44:30 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Wed, 12 Jun 2024 21:40:13 +0200 |
wenzelm |
minor performance tuning;
|
changeset |
files
|
| Wed, 12 Jun 2024 16:58:55 +0200 |
wenzelm |
proper sha1_digest: need to include offset + length;
|
changeset |
files
|
| Tue, 11 Jun 2024 21:32:26 +0200 |
wenzelm |
clarified signature: pro-forma support for Bytes with size: Long;
|
changeset |
files
|
| Tue, 11 Jun 2024 16:48:20 +0200 |
wenzelm |
minor performance tuning;
|
changeset |
files
|
| Tue, 11 Jun 2024 16:39:53 +0200 |
wenzelm |
clarified signature (again);
|
changeset |
files
|
| Tue, 11 Jun 2024 16:37:17 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 11 Jun 2024 16:32:10 +0200 |
wenzelm |
clarified signature: discontinue somewhat misleading Bytes <: CharSequence;
|
changeset |
files
|
| Tue, 11 Jun 2024 16:02:33 +0200 |
wenzelm |
minor performance tuning;
|
changeset |
files
|
| Tue, 11 Jun 2024 15:49:39 +0200 |
wenzelm |
clarified signature: more accurate types;
|
changeset |
files
|
| Tue, 11 Jun 2024 14:18:19 +0200 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Wed, 12 Jun 2024 10:47:53 +0200 |
Fabian Huch |
tuned messages;
|
changeset |
files
|
| Wed, 12 Jun 2024 08:52:36 +0200 |
Fabian Huch |
clarified web server paths;
|
changeset |
files
|
| Tue, 11 Jun 2024 14:27:04 +0200 |
Fabian Huch |
sort web app parameters in list;
|
changeset |
files
|
| Tue, 11 Jun 2024 11:07:48 +0200 |
Fabian Huch |
proper available hosts;
|
changeset |
files
|
| Tue, 11 Jun 2024 10:27:35 +0200 |
desharna |
tuned proof
|
changeset |
files
|
| Tue, 11 Jun 2024 10:30:55 +0200 |
Fabian Huch |
tuned comments;
|
changeset |
files
|
| Tue, 11 Jun 2024 08:58:22 +0200 |
Fabian Huch |
add build_manager_database tool to restore db from log files;
|
changeset |
files
|
| Mon, 10 Jun 2024 18:45:21 +0200 |
Fabian Huch |
use build log in build manager to store meta-data persistently;
|
changeset |
files
|
| Mon, 10 Jun 2024 18:45:12 +0200 |
Fabian Huch |
add build log format for managed builds;
|
changeset |
files
|
| Mon, 10 Jun 2024 17:08:47 +0200 |
Fabian Huch |
improve build manager log (for build_log);
|
changeset |
files
|
| Mon, 10 Jun 2024 16:37:16 +0200 |
Fabian Huch |
clarified;
|
changeset |
files
|
| Mon, 10 Jun 2024 16:14:44 +0200 |
Fabian Huch |
proper web server address;
|
changeset |
files
|
| Mon, 10 Jun 2024 16:02:53 +0200 |
Fabian Huch |
clarified names: more canonical;
|
changeset |
files
|
| Mon, 10 Jun 2024 15:13:21 +0200 |
Fabian Huch |
clarified;
|
changeset |
files
|
| Mon, 10 Jun 2024 14:08:15 +0200 |
Fabian Huch |
remove unused;
|
changeset |
files
|
| Mon, 10 Jun 2024 14:03:19 +0200 |
Fabian Huch |
tuned;
|
changeset |
files
|
| Tue, 11 Jun 2024 08:02:13 +0200 |
desharna |
fixed NEWS
|
changeset |
files
|
| Mon, 10 Jun 2024 23:24:33 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Mon, 10 Jun 2024 20:23:42 +0200 |
wenzelm |
tuned signature: more exports;
|
changeset |
files
|
| Mon, 10 Jun 2024 14:53:54 +0200 |
wenzelm |
clarified signature: prefer internal Thm_Name.T over external Facts.ref;
|
changeset |
files
|
| Mon, 10 Jun 2024 14:29:33 +0200 |
wenzelm |
more robust / permissive;
|
changeset |
files
|
| Mon, 10 Jun 2024 14:05:39 +0200 |
wenzelm |
clarified signature: more operations;
|
changeset |
files
|
| Mon, 10 Jun 2024 14:04:52 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 10 Jun 2024 12:44:49 +0200 |
wenzelm |
clarified operations, following pretty_thm_name;
|
changeset |
files
|
| Mon, 10 Jun 2024 12:07:54 +0200 |
wenzelm |
more accurate treatment of Thm_Name.T;
|
changeset |
files
|
| Mon, 10 Jun 2024 21:32:24 +0200 |
desharna |
renamed lemmas
|
changeset |
files
|
| Mon, 10 Jun 2024 18:10:09 +0200 |
desharna |
merged
|
changeset |
files
|
| Mon, 10 Jun 2024 14:09:55 +0200 |
desharna |
renamed theorems
|
changeset |
files
|
| Mon, 10 Jun 2024 13:44:46 +0200 |
desharna |
renamed theorems
|
changeset |
files
|
| Mon, 10 Jun 2024 13:55:59 +0200 |
Fabian Huch |
add title;
|
changeset |
files
|
| Mon, 10 Jun 2024 13:45:12 +0200 |
Fabian Huch |
use build_cluster in ci builds;
|
changeset |
files
|
| Mon, 10 Jun 2024 13:39:09 +0200 |
desharna |
merged
|
changeset |
files
|
| Mon, 10 Jun 2024 08:34:09 +0200 |
desharna |
tuned alias names in formulas
|
changeset |
files
|
| Mon, 10 Jun 2024 08:25:55 +0200 |
desharna |
renamed theorems
|
changeset |
files
|
| Fri, 07 Jun 2024 19:14:36 +0200 |
Fabian Huch |
add favicon to web app;
|
changeset |
files
|
| Sun, 09 Jun 2024 22:40:13 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Sun, 09 Jun 2024 21:16:38 +0200 |
wenzelm |
clarified data representation: prefer explicit type Thm_Name;
|
changeset |
files
|
| Sun, 09 Jun 2024 21:15:27 +0200 |
wenzelm |
more operations, following Isabelle/ML;
|
changeset |
files
|
| Sun, 09 Jun 2024 20:47:30 +0200 |
wenzelm |
clarified signature: more explicit operations;
|
changeset |
files
|
| Sun, 09 Jun 2024 20:37:39 +0200 |
wenzelm |
clarified treatment of Thm_Name.T (again, see also 8a9588ffc133);
|
changeset |
files
|
| Sun, 09 Jun 2024 20:19:53 +0200 |
wenzelm |
clarified operations, including exceptions;
|
changeset |
files
|
| Sun, 09 Jun 2024 20:04:41 +0200 |
wenzelm |
tuned: more direct Isabelle/ML;
|
changeset |
files
|
| Sun, 09 Jun 2024 19:49:42 +0200 |
wenzelm |
clarified modules;
|
changeset |
files
|
| Sun, 09 Jun 2024 15:31:33 +0200 |
wenzelm |
more accurate thm "name_hint", using Thm_Name.T;
|
changeset |
files
|
| Sun, 09 Jun 2024 15:11:07 +0200 |
wenzelm |
more operationsd;
|
changeset |
files
|
| Sun, 09 Jun 2024 12:29:04 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 08 Jun 2024 23:17:20 +0200 |
wenzelm |
more robust: prefer synchronous compression (usually <= 1ms, sometimes 1..5ms);
|
changeset |
files
|
| Sat, 08 Jun 2024 19:47:14 +0200 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Sat, 08 Jun 2024 19:43:08 +0200 |
wenzelm |
clarified output, following Consumer_Thread.failure;
|
changeset |
files
|
| Sat, 08 Jun 2024 19:35:28 +0200 |
wenzelm |
more informative exception output, with optional trace;
|
changeset |
files
|
| Sat, 08 Jun 2024 16:26:47 +0200 |
wenzelm |
more accurate output of Thm_Name.T wrt. facts name space;
|
changeset |
files
|
| Sat, 08 Jun 2024 11:47:48 +0200 |
wenzelm |
clarified signature: more operations;
|
changeset |
files
|
| Sat, 08 Jun 2024 11:32:38 +0200 |
wenzelm |
tuned structure;
|
changeset |
files
|
| Sat, 08 Jun 2024 11:23:40 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 07 Jun 2024 23:53:31 +0200 |
wenzelm |
more accurate Thm_Name.T for PThm / Thm.name_derivation / Thm.derivation_name;
|
changeset |
files
|
| Fri, 07 Jun 2024 15:20:01 +0200 |
wenzelm |
clarified signature: prefer explicit operation;
|
changeset |
files
|
| Fri, 07 Jun 2024 15:01:16 +0200 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Fri, 07 Jun 2024 13:46:51 +0200 |
wenzelm |
tuned: prefer Thm_Name operations;
|
changeset |
files
|
| Fri, 07 Jun 2024 13:40:12 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 07 Jun 2024 13:37:20 +0200 |
wenzelm |
prefer dynamic position from command transaction;
|
changeset |
files
|
| Fri, 07 Jun 2024 13:19:39 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Fri, 07 Jun 2024 12:39:14 +0200 |
wenzelm |
clarified signature: more explicit preprocessing;
|
changeset |
files
|
| Fri, 07 Jun 2024 11:44:15 +0200 |
wenzelm |
clarified signature: separate formal context from exported theory_name;
|
changeset |
files
|
| Fri, 07 Jun 2024 11:10:49 +0200 |
wenzelm |
tuned signature: just one ZThm is sufficient;
|
changeset |
files
|
| Sat, 08 Jun 2024 14:57:14 +0200 |
desharna |
renamed lemmas
|
changeset |
files
|
| Fri, 07 Jun 2024 18:50:46 +0200 |
Fabian Huch |
build manager: echo error messages to server output;
|
changeset |
files
|
| Fri, 07 Jun 2024 18:16:50 +0200 |
Fabian Huch |
omit showing previous failures for user builds;
|
changeset |
files
|
| Fri, 07 Jun 2024 17:40:12 +0200 |
Fabian Huch |
always handle interrupted jobs;
|
changeset |
files
|
| Fri, 07 Jun 2024 15:47:19 +0200 |
Fabian Huch |
add cluster/hosts configurations to build manager: allows running jobs in parallel on distinct hardware;
|
changeset |
files
|
| Fri, 07 Jun 2024 15:04:07 +0200 |
Fabian Huch |
clarified context: operations now in build process;
|
changeset |
files
|
| Fri, 07 Jun 2024 14:00:59 +0200 |
Fabian Huch |
clarified: add explicit build process;
|
changeset |
files
|
| Fri, 07 Jun 2024 13:54:00 +0200 |
Fabian Huch |
remove unnecessary subdir;
|
changeset |
files
|
| Fri, 07 Jun 2024 13:52:25 +0200 |
Fabian Huch |
tuned;
|
changeset |
files
|
| Thu, 06 Jun 2024 23:19:59 +0200 |
wenzelm |
tuned proof: avoid smt/z3 to make this work with arm64-linux;
|
changeset |
files
|
| Thu, 06 Jun 2024 23:12:04 +0200 |
wenzelm |
proper afp_directory (amending 9308bc5f65d6);
|
changeset |
files
|
| Thu, 06 Jun 2024 22:26:40 +0200 |
wenzelm |
clarified names;
|
changeset |
files
|
| Thu, 06 Jun 2024 22:34:24 +0200 |
wenzelm |
clarified name: avoid clash with Library.Update;
|
changeset |
files
|
| Thu, 06 Jun 2024 22:13:10 +0200 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Thu, 06 Jun 2024 22:03:20 +0200 |
wenzelm |
tuned whitespace;
|
changeset |
files
|
| Thu, 06 Jun 2024 21:48:36 +0200 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Thu, 06 Jun 2024 21:13:51 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Thu, 06 Jun 2024 12:53:02 +0200 |
wenzelm |
more informative ZBox;
|
changeset |
files
|
| Thu, 06 Jun 2024 12:42:42 +0200 |
wenzelm |
more operations;
|
changeset |
files
|
| Thu, 06 Jun 2024 11:53:52 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Thu, 06 Jun 2024 11:41:15 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 06 Jun 2024 11:32:39 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Wed, 05 Jun 2024 11:30:26 +0200 |
wenzelm |
remove unused (see also 04214caeb9ac);
|
changeset |
files
|
| Tue, 04 Jun 2024 15:13:26 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Thu, 06 Jun 2024 14:51:28 +0200 |
Fabian Huch |
add triggers to ci jobs: on commit vs timed;
|
changeset |
files
|
| Thu, 06 Jun 2024 13:37:27 +0200 |
Fabian Huch |
manage components of ci builds;
|
changeset |
files
|
| Thu, 06 Jun 2024 09:04:01 +0200 |
Fabian Huch |
use external CSS for build manager page;
|
changeset |
files
|
| Thu, 06 Jun 2024 08:58:58 +0200 |
Fabian Huch |
more build manager page;
|
changeset |
files
|
| Wed, 05 Jun 2024 20:09:04 +0200 |
Fabian Huch |
more page elements;
|
changeset |
files
|
| Wed, 05 Jun 2024 20:06:34 +0200 |
Fabian Huch |
web app: add automatic resize;
|
changeset |
files
|
| Wed, 05 Jun 2024 17:41:16 +0200 |
Fabian Huch |
ensure permissions when starting build task (e.g., due to misconfigured client);
|
changeset |
files
|
| Wed, 05 Jun 2024 17:27:13 +0200 |
Fabian Huch |
add verbose option to build_task;
|
changeset |
files
|
| Wed, 05 Jun 2024 15:01:31 +0200 |
Fabian Huch |
tuned;
|
changeset |
files
|
| Wed, 05 Jun 2024 15:01:20 +0200 |
Fabian Huch |
build manager: manage directories/permissions, to minimize local administration;
|
changeset |
files
|
| Tue, 04 Jun 2024 18:55:55 +0200 |
Fabian Huch |
read prefs properly;
|
changeset |
files
|
| Tue, 04 Jun 2024 18:43:04 +0200 |
Fabian Huch |
allow explicit Isabelle rev in build task (e.g., for older Isabelle versions);
|
changeset |
files
|
| Tue, 04 Jun 2024 18:24:38 +0200 |
Fabian Huch |
web app: proper document height;
|
changeset |
files
|
| Tue, 04 Jun 2024 18:08:47 +0200 |
nipkow |
merged
|
changeset |
files
|
| Tue, 04 Jun 2024 11:21:04 +0200 |
nipkow |
replace manual def. of timing function
|
changeset |
files
|
| Tue, 04 Jun 2024 09:02:36 +0200 |
Fabian Huch |
add build manager module;
|
changeset |
files
|
| Tue, 04 Jun 2024 09:02:18 +0200 |
Fabian Huch |
support ci job via hg_sync (cf. 7883f221d6d3);
|
changeset |
files
|
| Mon, 03 Jun 2024 19:37:42 +0200 |
Fabian Huch |
tuned;
|
changeset |
files
|
| Mon, 03 Jun 2024 19:21:22 +0200 |
Fabian Huch |
use Content-Digest header in HEAD requests instead of length (to track non-monotone changes);
|
changeset |
files
|
| Mon, 03 Jun 2024 20:56:41 +0100 |
paulson |
merged
|
changeset |
files
|
| Mon, 03 Jun 2024 20:56:21 +0100 |
paulson |
Simplification of sin, cos, exp of multiples of pi
|
changeset |
files
|
| Mon, 03 Jun 2024 20:28:25 +0200 |
wenzelm |
minor performance tuning: more compact data;
|
changeset |
files
|
| Mon, 03 Jun 2024 19:43:21 +0200 |
wenzelm |
removed unused/inefficient size_of_proof (see also 2241191a3c54);
|
changeset |
files
|
| Sun, 02 Jun 2024 14:11:09 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 02 Jun 2024 13:36:24 +0200 |
wenzelm |
more robust: avoid crash of sleep() for negative time;
|
changeset |
files
|
| Sat, 01 Jun 2024 21:52:31 +0200 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Sat, 01 Jun 2024 21:49:50 +0200 |
wenzelm |
clarified signature: more explicit types;
|
changeset |
files
|
| Sat, 01 Jun 2024 16:26:35 +0200 |
wenzelm |
support "rsync --chmod --chown" via Rsync.Context;
|
changeset |
files
|
| Sat, 01 Jun 2024 16:19:14 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 01 Jun 2024 15:22:37 +0200 |
wenzelm |
bash: proper bash_process via SSH;
|
changeset |
files
|
| Sat, 01 Jun 2024 15:13:03 +0200 |
wenzelm |
clarified signature: support explicit cwd;
|
changeset |
files
|
| Sat, 01 Jun 2024 15:11:46 +0200 |
wenzelm |
support bash via SSH;
|
changeset |
files
|
| Sat, 01 Jun 2024 15:03:13 +0200 |
wenzelm |
clarified comments;
|
changeset |
files
|
| Sat, 01 Jun 2024 14:56:24 +0200 |
wenzelm |
proper support for remote cwd;
|
changeset |
files
|
| Sat, 01 Jun 2024 14:33:38 +0200 |
wenzelm |
clarified context for (remote) bash scripts: export variables are optional, support cwd;
|
changeset |
files
|
| Sat, 01 Jun 2024 14:08:04 +0200 |
wenzelm |
more operations for SSH.System: bash_process and bash;
|
changeset |
files
|
| Sat, 01 Jun 2024 12:35:38 +0200 |
wenzelm |
unused;
|
changeset |
files
|
| Sat, 01 Jun 2024 12:31:06 +0200 |
wenzelm |
clarified signature: prefer symbolic isabelle.Path over physical java.io.File;
|
changeset |
files
|
| Fri, 31 May 2024 22:35:44 +0200 |
wenzelm |
minor performance tuning;
|
changeset |
files
|
| Fri, 31 May 2024 22:19:31 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Fri, 31 May 2024 22:10:11 +0200 |
wenzelm |
minor performance tuning: save approx. 70ms per SSH command;
|
changeset |
files
|
| Fri, 31 May 2024 21:39:01 +0200 |
wenzelm |
minor performance tuning: save approx. 70ms per SSH command;
|
changeset |
files
|
| Fri, 31 May 2024 21:17:01 +0200 |
wenzelm |
minor performance tuning: save approx. 70ms per SSH test command;
|
changeset |
files
|
| Fri, 31 May 2024 20:46:51 +0200 |
wenzelm |
suport Isabelle_System.bash via SSH.System;
|
changeset |
files
|
| Fri, 31 May 2024 15:56:41 +0200 |
wenzelm |
more operations;
|
changeset |
files
|
| Fri, 31 May 2024 15:38:28 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 31 May 2024 15:26:17 +0200 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Fri, 31 May 2024 14:17:28 +0200 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Wed, 29 May 2024 16:16:29 +0200 |
wenzelm |
obsolete: macOS 10.x is no longer supported (see also 059743bc8311);
|
changeset |
files
|
| Wed, 29 May 2024 16:08:17 +0200 |
wenzelm |
tuned tmp name;
|
changeset |
files
|
| Wed, 29 May 2024 16:06:07 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 29 May 2024 15:58:03 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 29 May 2024 15:51:15 +0200 |
wenzelm |
tuned comments;
|
changeset |
files
|
| Wed, 29 May 2024 18:13:05 +0200 |
nipkow |
merged
|
changeset |
files
|
| Wed, 29 May 2024 10:43:22 +0200 |
nipkow |
pretty-printing sledgehammer command: merge indexed theorems
|
changeset |
files
|
| Wed, 29 May 2024 16:23:48 +0200 |
Fabian Huch |
clarify routes: absolute in api and relative for frontend;
|
changeset |
files
|
| Wed, 29 May 2024 15:09:48 +0200 |
Fabian Huch |
add auto-reload for more interactive web apps;
|
changeset |
files
|
| Wed, 29 May 2024 14:55:36 +0200 |
Fabian Huch |
clarified web app endpoints;
|
changeset |
files
|
| Tue, 28 May 2024 19:51:49 +0200 |
Fabian Huch |
proper html script tag: source code must not be escaped;
|
changeset |
files
|
| Tue, 28 May 2024 19:51:09 +0200 |
Fabian Huch |
add explicit Content-Length header to http response (otherwise it is missing in HEAD responses);
|
changeset |
files
|
| Tue, 28 May 2024 19:49:42 +0200 |
Fabian Huch |
add HEAD to http server: should send same header fields as if request was GET;
|
changeset |
files
|
| Sat, 25 May 2024 20:26:06 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 25 May 2024 20:10:17 +0200 |
wenzelm |
tuned spelling;
|
changeset |
files
|
| Sat, 25 May 2024 20:08:01 +0200 |
wenzelm |
support direct rsync from Hg_Sync result directory (usually requires option -d "~~/dirs");
|
changeset |
files
|
| Sat, 25 May 2024 19:42:09 +0200 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Sat, 25 May 2024 17:22:05 +0200 |
wenzelm |
more general dirs for Sync.sync;
|
changeset |
files
|
| Sat, 25 May 2024 12:20:57 +0200 |
wenzelm |
tuned whitespace (amending beb4ee344c22);
|
changeset |
files
|
| Sat, 25 May 2024 12:09:37 +0200 |
wenzelm |
clarified signature (see also be0ab4b94c62 and c41791ad75c3);
|
changeset |
files
|
| Fri, 24 May 2024 20:23:14 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 24 May 2024 19:15:51 +0200 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Fri, 24 May 2024 17:31:49 +0200 |
wenzelm |
tuned names;
|
changeset |
files
|
| Fri, 24 May 2024 17:14:02 +0200 |
wenzelm |
proper SSH.System operation;
|
changeset |
files
|
| Fri, 24 May 2024 17:06:57 +0200 |
wenzelm |
clarified modules;
|
changeset |
files
|
| Fri, 24 May 2024 16:15:27 +0200 |
wenzelm |
more uniform/robust detect_repository/is_repository: actually check hg root;
|
changeset |
files
|
| Fri, 24 May 2024 15:55:34 +0200 |
wenzelm |
more uniform local/remote operations;
|
changeset |
files
|
| Thu, 23 May 2024 21:39:40 +0200 |
wenzelm |
disable Isabelle/Naproche after release;
|
changeset |
files
|
| Thu, 23 May 2024 20:24:26 +0200 |
wenzelm |
post-release updates;
|
changeset |
files
|
| Thu, 23 May 2024 20:22:52 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Thu, 23 May 2024 11:18:46 +0200 |
wenzelm |
Added tag Isabelle2024 for changeset 29f2b8ff84f3
|
changeset |
files
|
| Mon, 20 May 2024 15:43:51 +0200 |
wenzelm |
proper support for "isabelle update -D DIR": avoid accidental exclusion of select_dirs (amending e5dafe9e120f);
Isabelle2024
|
changeset |
files
|
| Sun, 19 May 2024 18:43:45 +0200 |
wenzelm |
provide scala-3.4.2, but do not activate it: scala-3.3.x is LTS version;
|
changeset |
files
|
| Sun, 19 May 2024 15:49:21 +0200 |
wenzelm |
update to naproche-20240519;
|
changeset |
files
|
| Sun, 12 May 2024 14:45:29 +0200 |
wenzelm |
proper formatting;
|
changeset |
files
|
| Sun, 12 May 2024 14:41:13 +0200 |
wenzelm |
more documentation on "isabelle build -H" and underlying system registry tables "host" and "cluster";
|
changeset |
files
|
| Mon, 13 May 2024 22:42:40 +0100 |
paulson |
More binomial material
|
changeset |
files
|
| Sun, 12 May 2024 23:23:39 +0100 |
paulson |
syntax of gchoose now the same as choose
|
changeset |
files
|
| Mon, 06 May 2024 14:39:33 +0100 |
paulson |
Some new simprules – and patches for proofs
|
changeset |
files
|
| Sun, 05 May 2024 15:31:08 +0100 |
paulson |
merged
|
changeset |
files
|
| Tue, 30 Apr 2024 19:55:19 +0100 |
paulson |
merged
|
changeset |
files
|
| Tue, 30 Apr 2024 13:23:47 +0100 |
paulson |
A little more tidying in Nominal
|
changeset |
files
|
| Fri, 03 May 2024 00:24:57 +0200 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Fri, 03 May 2024 00:07:51 +0200 |
wenzelm |
merged, resoving conflicts in src/HOL/Nominal/Nominal.thy;
|
changeset |
files
|
| Thu, 02 May 2024 15:40:05 +0200 |
wenzelm |
Added tag Isabelle2024-RC3 for changeset 007e6af8a020
|
changeset |
files
|
| Thu, 02 May 2024 14:08:59 +0200 |
wenzelm |
more documentation on "System registry via TOML";
|
changeset |
files
|
| Thu, 02 May 2024 04:38:10 +0200 |
wenzelm |
update to naproche-20240502: proper platform_path for NAPROCHE_FORMALIZATIONS to make it work on Windows;
|
changeset |
files
|
| Wed, 01 May 2024 20:26:20 +0200 |
wenzelm |
provide 3.1 for testing (inactive);
|
changeset |
files
|
| Wed, 01 May 2024 20:12:58 +0200 |
wenzelm |
build e-3.1, without patch;
|
changeset |
files
|
| Wed, 01 May 2024 20:11:36 +0200 |
wenzelm |
disable Isabelle/Naproche for now: does not quite work on Windows;
|
changeset |
files
|
| Wed, 01 May 2024 16:16:05 +0200 |
wenzelm |
update and activate naproche component for release;
|
changeset |
files
|
| Mon, 29 Apr 2024 14:50:10 +0200 |
desharna |
changed URL to SystemOnTPTP at Geoff's request
|
changeset |
files
|
| Mon, 29 Apr 2024 12:22:06 +0200 |
wenzelm |
tuned spelling;
|
changeset |
files
|
| Sun, 28 Apr 2024 14:28:36 +0200 |
wenzelm |
build_cluster always uses build_database_server for now -- despite 1fa1b32b0379: its local/remote storage model often leads to incoherent state;
|
changeset |
files
|
| Fri, 26 Apr 2024 21:32:27 +0200 |
wenzelm |
proper directory permissions to make "rm" work, notably for cygwin/etc/pki/ca-trust/extracted/pem/directory-hash;
|
changeset |
files
|
| Fri, 26 Apr 2024 20:18:15 +0200 |
wenzelm |
support more Ubuntu versions;
|
changeset |
files
|
| Fri, 26 Apr 2024 20:14:27 +0200 |
wenzelm |
updated for release;
|
changeset |
files
|
| Fri, 26 Apr 2024 19:15:37 +0200 |
wenzelm |
more robust: avoid spurious ConcurrentModificationException;
|
changeset |
files
|
| Wed, 24 Apr 2024 20:41:35 +0200 |
wenzelm |
update to e-3.0.03-1, with proper support for trivial statements;
|
changeset |
files
|
| Wed, 24 Apr 2024 20:05:25 +0200 |
wenzelm |
more robust;
|
changeset |
files
|
| Wed, 24 Apr 2024 19:48:45 +0200 |
wenzelm |
minor patch for E Prover, based on "git diff -w -r E-3.0.03 E-3.0.08": proper support for trivial statements;
|
changeset |
files
|
| Sat, 20 Apr 2024 17:10:34 +0200 |
wenzelm |
backed out changeset 601ff5c7cad5: not relevant for Isabelle2024;
|
changeset |
files
|
| Sat, 20 Apr 2024 16:07:00 +0200 |
wenzelm |
clone of 0c51e0a6bc37;
|
changeset |
files
|
| Fri, 26 Apr 2024 13:25:44 +0200 |
wenzelm |
update Windows test machines;
|
changeset |
files
|
| Wed, 24 Apr 2024 20:56:26 +0100 |
paulson |
More tidying of proofs
|
changeset |
files
|
| Wed, 24 Apr 2024 09:21:44 +0100 |
paulson |
Another Nominal example
|
changeset |
files
|
| Tue, 23 Apr 2024 21:58:42 +0100 |
paulson |
merged
|
changeset |
files
|
| Tue, 23 Apr 2024 21:58:21 +0100 |
paulson |
Tidying up another Nominal example (SOS)
|
changeset |
files
|
| Tue, 23 Apr 2024 15:57:03 +0200 |
wenzelm |
update Windows build host;
|
changeset |
files
|
| Tue, 23 Apr 2024 15:56:04 +0200 |
wenzelm |
proper command-line;
|
changeset |
files
|
| Tue, 23 Apr 2024 10:26:04 +0100 |
paulson |
Tidying up another of the nominal examples
|
changeset |
files
|
| Mon, 22 Apr 2024 22:08:28 +0100 |
paulson |
More tidying of Nominal proofs
|
changeset |
files
|
| Mon, 22 Apr 2024 10:43:57 +0100 |
paulson |
Tidied up another messy theory
|
changeset |
files
|
| Sun, 21 Apr 2024 16:31:30 +0100 |
paulson |
More proof tidying for Nominal
|
changeset |
files
|
| Sat, 20 Apr 2024 23:02:47 +0100 |
paulson |
Tidying up more messy proofs
|
changeset |
files
|
| Sat, 20 Apr 2024 12:08:01 +0100 |
paulson |
Starting to tidy HOL-Nominal-Examples
|
changeset |
files
|
| Thu, 18 Apr 2024 17:53:14 +0200 |
Simon Wimmer |
sketch & explore: recover from duplicate fixed variables in Isar proofs
|
changeset |
files
|
| Thu, 18 Apr 2024 13:06:48 +0200 |
wenzelm |
back to post-release mode -- after fork point;
|
changeset |
files
|
| Thu, 18 Apr 2024 15:20:24 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Thu, 18 Apr 2024 11:39:51 +0200 |
wenzelm |
Added tag Isabelle2024-RC2 for changeset ef2134570abb
|
changeset |
files
|
| Thu, 18 Apr 2024 13:07:34 +0100 |
paulson |
Acknowledgement of Ata Keskin for his Martingales material
|
changeset |
files
|
| Wed, 17 Apr 2024 23:22:32 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 17 Apr 2024 23:12:21 +0200 |
wenzelm |
update to jdk-21.0.3;
|
changeset |
files
|
| Wed, 17 Apr 2024 22:07:21 +0100 |
paulson |
merged
|
changeset |
files
|
| Wed, 17 Apr 2024 22:07:07 +0100 |
paulson |
Tidied up horrible archaic proofs
|
changeset |
files
|
| Wed, 17 Apr 2024 21:20:31 +0200 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Wed, 17 Apr 2024 15:04:27 +0200 |
Kevin Kappelmann |
make adhoc_overloading respect type constraints
|
changeset |
files
|
| Tue, 16 Apr 2024 17:28:58 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Tue, 16 Apr 2024 17:06:05 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 16 Apr 2024 16:54:15 +0200 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Tue, 16 Apr 2024 16:38:54 +0200 |
wenzelm |
minor performance tuning: avoid redundant server access;
|
changeset |
files
|
| Tue, 16 Apr 2024 16:37:08 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 16 Apr 2024 16:53:10 +0200 |
wenzelm |
clarified modules and options (from store);
|
changeset |
files
|
| Tue, 16 Apr 2024 16:27:40 +0200 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Tue, 16 Apr 2024 15:14:55 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 16 Apr 2024 15:11:13 +0200 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Tue, 16 Apr 2024 14:48:08 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Tue, 16 Apr 2024 12:18:32 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 16 Apr 2024 12:08:40 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Tue, 16 Apr 2024 11:39:02 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 16 Apr 2024 11:20:30 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 16 Apr 2024 11:00:46 +0200 |
wenzelm |
more robust tmp_file (see also ab07d4cb7d1c and 146468e05dd4);
|
changeset |
files
|
| Fri, 12 Apr 2024 17:07:33 +0200 |
wenzelm |
tuned messages;
|
changeset |
files
|
| Thu, 11 Apr 2024 12:12:33 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 11 Apr 2024 12:05:01 +0200 |
wenzelm |
back to static numa_nodes (reverting part of c2c59de57df9);
|
changeset |
files
|
| Thu, 11 Apr 2024 12:04:44 +0200 |
wenzelm |
tuned messages;
|
changeset |
files
|
| Tue, 16 Apr 2024 13:29:27 +0200 |
Manuel Eberl |
canonical time function for List.nth
|
changeset |
files
|
| Mon, 15 Apr 2024 22:24:31 +0100 |
paulson |
merged
|
changeset |
files
|
| Mon, 15 Apr 2024 22:23:40 +0100 |
paulson |
Streamlining of many more archaic proofs
|
changeset |
files
|
| Mon, 15 Apr 2024 20:35:56 +0200 |
Fabian Huch |
clarified web app parameters: more flexible, using HTML5 id specification (nonempty unicode string with no spaces);
|
changeset |
files
|
| Sun, 14 Apr 2024 22:38:17 +0100 |
paulson |
More tidying of old proofs
|
changeset |
files
|
| Sun, 14 Apr 2024 18:39:53 +0100 |
paulson |
merged
|
changeset |
files
|
| Sun, 14 Apr 2024 18:39:43 +0100 |
paulson |
More tidying and removal of "apply"
|
changeset |
files
|
| Sat, 13 Apr 2024 10:22:14 +0200 |
Simon Wimmer |
Add subgoals variant of 'sketch' command
|
changeset |
files
|
| Fri, 12 Apr 2024 22:19:27 +0100 |
paulson |
merged
|
changeset |
files
|
| Fri, 12 Apr 2024 22:19:20 +0100 |
paulson |
Tidied some messy proofs
|
changeset |
files
|
| Thu, 11 Apr 2024 18:46:49 +0000 |
haftmann |
prefer canonical theorem name for fact collection declarations
|
changeset |
files
|
| Fri, 12 Apr 2024 09:58:53 +0100 |
paulson |
merged
|
changeset |
files
|
| Fri, 12 Apr 2024 09:58:32 +0100 |
paulson |
Tidying ugly proofs
|
changeset |
files
|
| Fri, 12 Apr 2024 10:10:16 +0200 |
Fabian Huch |
tuned;
|
changeset |
files
|
| Thu, 11 Apr 2024 14:13:43 +0200 |
Manuel Eberl |
tweaked time functions for median-of-medians selection in HOL-Data_Structures
|
changeset |
files
|
| Wed, 10 Apr 2024 13:23:00 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 10 Apr 2024 11:44:25 +0200 |
wenzelm |
rename \undef to \undefined to avoid problems with MacTeX 2014 or Ubuntu 24.04 beta;
|
changeset |
files
|
| Wed, 10 Apr 2024 11:32:48 +0100 |
paulson |
Tiny tweaks to proofs
|
changeset |
files
|
| Mon, 08 Apr 2024 16:27:11 +0100 |
paulson |
A bit of new material about type class "infinite", from Eval_FO
|
changeset |
files
|
| Fri, 05 Apr 2024 21:21:02 +0200 |
wenzelm |
avoid Scala if-expressions and thus make it work both for -new-syntax or -old-syntax;
|
changeset |
files
|
| Fri, 05 Apr 2024 20:41:54 +0200 |
wenzelm |
proper Scala code for String.literal_of_asciis: avoid ambiguity of ("" ++ ...);
|
changeset |
files
|
| Fri, 05 Apr 2024 17:47:09 +0200 |
wenzelm |
adjust generated Scala to make it work with scalac -old-syntax and -new-syntax, although the latter is not regularly tested;
|
changeset |
files
|
| Fri, 05 Apr 2024 17:10:02 +0200 |
Simon Wimmer |
Add entry on Sketch_and_Explore to CONTRIBUTORS
|
changeset |
files
|
| 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
|
changeset |
files
|
| Thu, 04 Apr 2024 11:40:45 +0200 |
wenzelm |
more portable: prefer official JDBC operation DatabaseMetaData.getColumns();
|
changeset |
files
|
| Thu, 04 Apr 2024 11:21:52 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Wed, 03 Apr 2024 16:55:34 +0200 |
desharna |
documented new syntax for fBall and fBex
|
changeset |
files
|
| Wed, 03 Apr 2024 11:35:06 +0200 |
wenzelm |
updated for release;
|
changeset |
files
|
| Wed, 03 Apr 2024 11:11:23 +0200 |
wenzelm |
Added tag Isabelle2024-RC1 for changeset 1231a7fb2510
|
changeset |
files
|
| Wed, 03 Apr 2024 11:09:58 +0200 |
wenzelm |
misc tuning for release;
|
changeset |
files
|
| Wed, 03 Apr 2024 11:02:09 +0200 |
wenzelm |
update for release;
|
changeset |
files
|
| Tue, 02 Apr 2024 19:18:55 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Tue, 02 Apr 2024 19:10:22 +0200 |
wenzelm |
update to stack-2.15.5, stackage-lts-22.15;
|
changeset |
files
|
| Tue, 02 Apr 2024 18:29:14 +0200 |
wenzelm |
clarified names: discontinue odd convention from 3 decades ago;
|
changeset |
files
|
| Tue, 02 Apr 2024 17:20:09 +0200 |
wenzelm |
further performance tuning (after f906f7f83dae): interactive mode is closer to earlier approach with Lazy.value, which could be relevant with rather complex grammars under tight memory situations;
|
changeset |
files
|
| Tue, 02 Apr 2024 18:02:43 +0200 |
Manuel Eberl |
added documentation for meromorphicity etc. in HOL-Complex_Analysis
|
changeset |
files
|
| Tue, 02 Apr 2024 16:33:53 +0200 |
desharna |
merged
|
changeset |
files
|
| Tue, 02 Apr 2024 08:35:43 +0200 |
desharna |
merged
|
changeset |
files
|
| Thu, 28 Mar 2024 09:41:51 +0100 |
desharna |
added special syntax for FSet.Ball and FSet.Bex
|
changeset |
files
|
| Thu, 28 Mar 2024 09:40:58 +0100 |
desharna |
tuned proof
|
changeset |
files
|
| Wed, 27 Mar 2024 18:29:32 +0100 |
desharna |
tuned proofs of Equiv_Relations.equiv
|
changeset |
files
|
| Tue, 02 Apr 2024 11:26:04 +0200 |
Lars Hupel |
remove transitional (dummy) component list for Go
|
changeset |
files
|
| Mon, 01 Apr 2024 15:47:15 +0200 |
wenzelm |
clarified signature: prefer authentic cterm used in Simplifier, avoid potential re-certification in user-code;
|
changeset |
files
|
| Mon, 01 Apr 2024 15:37:55 +0200 |
wenzelm |
clarified names (see also 9c00a46d69d0, c5cd7a58cf2d);
|
changeset |
files
|
| Mon, 01 Apr 2024 15:09:30 +0200 |
wenzelm |
provide scala-3.4.1, but do not activate it: scala-3.3.x is LTS version;
|
changeset |
files
|
| Mon, 01 Apr 2024 14:36:28 +0200 |
wenzelm |
clarified "bulky" sessions (again, see also 06153e2e0cdb), but note that "very_slow" is normally used together with "slow";
|
changeset |
files
|
| Fri, 29 Mar 2024 19:28:59 +0100 |
Manuel Eberl |
moved over material from AFP; most importantly on algebraic numbers and algebraically closed fields
|
changeset |
files
|
| Sat, 30 Mar 2024 01:12:48 +0100 |
Fabian Huch |
update NEWS;
|
changeset |
files
|
| Sat, 30 Mar 2024 01:08:25 +0100 |
Fabian Huch |
moved web_app module from AFP (e.g., for building web services for the distributed build);
|
changeset |
files
|
| Thu, 28 Mar 2024 15:08:58 +0100 |
Fabian Huch |
tuned;
|
changeset |
files
|
| Thu, 28 Mar 2024 16:40:57 +0100 |
wenzelm |
removed unused/obsolete material: some of it was motivated by Isabelle/MMT (e.g. f150253cb201), but is superseded by AFP metadata (TOML);
|
changeset |
files
|
| Thu, 28 Mar 2024 16:38:12 +0100 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Thu, 28 Mar 2024 16:27:36 +0100 |
wenzelm |
clarified modules: more official Sessions.notable_groups;
|
changeset |
files
|
| Thu, 28 Mar 2024 16:14:28 +0100 |
nipkow |
tuned
|
changeset |
files
|
| Thu, 28 Mar 2024 13:33:10 +0000 |
paulson |
merged
|
changeset |
files
|
| Thu, 28 Mar 2024 13:32:57 +0000 |
paulson |
An assortment of new material, mostly due to Manuel
|
changeset |
files
|
| Thu, 28 Mar 2024 12:56:20 +0100 |
wenzelm |
rebuild rsync-3.2.7 on current platforms, including native arm64-darwin;
|
changeset |
files
|
| Thu, 28 Mar 2024 11:45:45 +0100 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Thu, 28 Mar 2024 11:35:39 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 28 Mar 2024 11:29:25 +0100 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Thu, 28 Mar 2024 08:30:42 +0100 |
desharna |
merged
|
changeset |
files
|
| Wed, 27 Mar 2024 11:49:42 +0100 |
desharna |
added lemma wfp_on_image and author name to theory
|
changeset |
files
|
| Wed, 27 Mar 2024 22:56:03 +0100 |
wenzelm |
proper ISABELLE_GO_SETUP, e.g. for AFP/Go compiler tests;
|
changeset |
files
|
| Wed, 27 Mar 2024 22:12:37 +0100 |
wenzelm |
proper "isabelle go_setup" for Jenkins;
|
changeset |
files
|
| Wed, 27 Mar 2024 21:51:03 +0100 |
wenzelm |
dummy Admin/components/go to avoid crash of Jenkins (see 38bbc2ff3c24);
|
changeset |
files
|
| Wed, 27 Mar 2024 17:51:37 +0100 |
wenzelm |
tuned message;
|
changeset |
files
|
| Wed, 27 Mar 2024 17:39:46 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 27 Mar 2024 17:39:28 +0100 |
wenzelm |
tuned NEWS;
|
changeset |
files
|
| Wed, 27 Mar 2024 17:11:46 +0100 |
wenzelm |
support for "all" platforms;
|
changeset |
files
|
| Wed, 27 Mar 2024 17:04:37 +0100 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Wed, 27 Mar 2024 16:48:36 +0100 |
nipkow |
merged
|
changeset |
files
|
| Wed, 27 Mar 2024 16:48:23 +0100 |
nipkow |
updated time functions for Array_Braun
|
changeset |
files
|
| Wed, 27 Mar 2024 15:16:21 +0000 |
paulson |
merged
|
changeset |
files
|
| Wed, 27 Mar 2024 15:16:09 +0000 |
paulson |
New material and a bit of refactoring
|
changeset |
files
|
| Wed, 27 Mar 2024 15:38:41 +0100 |
wenzelm |
remove unused TEMP_WINDOWS more thoroughly (see also fa18208fd7bd and 37f852399a32);
|
changeset |
files
|
| Wed, 27 Mar 2024 15:01:38 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 27 Mar 2024 14:40:02 +0100 |
wenzelm |
more robust Markdown;
|
changeset |
files
|
| Wed, 27 Mar 2024 14:37:52 +0100 |
wenzelm |
misc tuning;
|
changeset |
files
|
| Wed, 27 Mar 2024 14:20:06 +0100 |
wenzelm |
run "isabelle components_build -u";
|
changeset |
files
|
| Wed, 27 Mar 2024 13:41:08 +0100 |
wenzelm |
remove obsolete component (see 8347ffa1f92c): superseded by "isabelle go_setup";
|
changeset |
files
|
| Wed, 27 Mar 2024 13:32:30 +0100 |
wenzelm |
tuned order;
|
changeset |
files
|
| Wed, 27 Mar 2024 13:23:15 +0100 |
wenzelm |
more Setup_Tool services;
|
changeset |
files
|
| Wed, 27 Mar 2024 13:19:21 +0100 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Wed, 27 Mar 2024 13:17:22 +0100 |
wenzelm |
proper SSH operations;
|
changeset |
files
|
| Wed, 27 Mar 2024 13:17:04 +0100 |
wenzelm |
tuned signature: more permissive;
|
changeset |
files
|
| Wed, 27 Mar 2024 12:54:43 +0100 |
wenzelm |
clarified signature: explicit variable is easier to find in source;
|
changeset |
files
|
| Wed, 27 Mar 2024 12:50:37 +0100 |
wenzelm |
proper services for Setup_Tool --- avoid hardwired stuff;
|
changeset |
files
|
| Wed, 27 Mar 2024 10:54:47 +0100 |
desharna |
merged
|
changeset |
files
|
| Tue, 26 Mar 2024 09:33:33 +0100 |
desharna |
renamed lemma wfP_iff_ex_minimal to wfp_iff_ex_minimal
|
changeset |
files
|
| Tue, 26 Mar 2024 21:44:18 +0100 |
wenzelm |
more robust XML body: allow empty text, as well as arbitrary pro-forma markup (e.g. see XML.blob in Isabelle/ML);
|
changeset |
files
|
| Tue, 26 Mar 2024 21:34:08 +0100 |
wenzelm |
more robust: untyped/unscoped markup elements need to reside in module Markup for minimal static checking (see also 11a1f4d7af51);
|
changeset |
files
|
| Tue, 26 Mar 2024 21:25:35 +0100 |
wenzelm |
misc tuning for release;
|
changeset |
files
|
| Tue, 26 Mar 2024 21:16:47 +0100 |
wenzelm |
merged;
|
changeset |
files
|
| Tue, 26 Mar 2024 21:09:46 +0100 |
wenzelm |
NEWS for "isabelle go_setup";
|
changeset |
files
|
| Tue, 26 Mar 2024 21:04:43 +0100 |
wenzelm |
proper platform_path for Windows;
|
changeset |
files
|
| Tue, 26 Mar 2024 20:58:01 +0100 |
wenzelm |
misc tuning, following go_setup;
|
changeset |
files
|
| Tue, 26 Mar 2024 20:39:06 +0100 |
wenzelm |
dynamic setup of Go component, similar to Dotnet;
|
changeset |
files
|
| Tue, 26 Mar 2024 20:23:13 +0100 |
wenzelm |
tuned comments;
|
changeset |
files
|
| Tue, 26 Mar 2024 17:27:35 +0100 |
wenzelm |
clarified signature: more operations;
|
changeset |
files
|
| Tue, 26 Mar 2024 17:06:23 +0100 |
wenzelm |
clarified signature: explicit type Platform.Info with derived operations;
|
changeset |
files
|
| Tue, 26 Mar 2024 16:04:06 +0100 |
wenzelm |
less ambitious parallelism: avoid exhaustion of memory (64GB total);
|
changeset |
files
|
| Tue, 26 Mar 2024 12:07:52 +0100 |
wenzelm |
provide ISABELLE_DOTNET_VERSION via settings, following "isabelle ghc_setup";
|
changeset |
files
|
| Tue, 26 Mar 2024 12:00:08 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 26 Mar 2024 11:45:49 +0100 |
wenzelm |
tuned messages;
|
changeset |
files
|
| Tue, 26 Mar 2024 11:32:16 +0100 |
wenzelm |
update to bash_process-20240326;
|
changeset |
files
|
| Tue, 26 Mar 2024 11:15:48 +0100 |
wenzelm |
build bash_process in Isabelle/Scala, with etc/platforms.prop to preserve all platform directories (e.g. for SSH upload);
|
changeset |
files
|
| Tue, 26 Mar 2024 10:30:41 +0100 |
wenzelm |
clarified meaning of platform.props: update on default;
|
changeset |
files
|
| Tue, 26 Mar 2024 16:01:54 +0100 |
Fabian Huch |
allow raw input in HTML (e.g., for web applications);
|
changeset |
files
|
| Tue, 26 Mar 2024 09:31:34 +0100 |
desharna |
added lemmas wfp_on_inv_imagep, wfp_on_if_convertible_to_wfp_on, and wf_on_if_convertible_to_wf_on
|
changeset |
files
|
| Tue, 26 Mar 2024 06:32:38 +0100 |
desharna |
merged
|
changeset |
files
|
| Mon, 25 Mar 2024 19:27:53 +0100 |
desharna |
added lemma wf_on_iff_wf
|
changeset |
files
|
| Mon, 25 Mar 2024 19:27:32 +0100 |
desharna |
changed number of consumed assumptions of wf_on_induct and wfp_on_induct
|
changeset |
files
|
| Mon, 25 Mar 2024 21:04:26 +0100 |
wenzelm |
obsolete: base-line is macOS 11;
|
changeset |
files
|
| Mon, 25 Mar 2024 20:55:27 +0100 |
wenzelm |
more robust: always assume x86_64 (or its emulation on ARM);
|
changeset |
files
|
| Mon, 25 Mar 2024 20:48:10 +0100 |
wenzelm |
MLton lacks arm64-linux (see also 84f2d481d6d7);
|
changeset |
files
|
| Mon, 25 Mar 2024 20:42:10 +0100 |
wenzelm |
more ambitious test "AFP (macOS 14 Sonoma, Apple Silicon)", as replacement for AFP on lrzcloud2;
|
changeset |
files
|
| Mon, 25 Mar 2024 20:22:05 +0100 |
wenzelm |
update to stack-2.15.3, stackage-lts-22.6, ghc-9.6.4;
|
changeset |
files
|
| Mon, 25 Mar 2024 20:05:40 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 25 Mar 2024 19:57:01 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Mon, 25 Mar 2024 19:56:12 +0100 |
wenzelm |
misc updates, tuning and clarification;
|
changeset |
files
|
| Mon, 25 Mar 2024 17:46:16 +0100 |
wenzelm |
reformat source in jEdit (wrap margin 78);
|
changeset |
files
|
| Mon, 25 Mar 2024 17:43:28 +0100 |
wenzelm |
more accurate Markdown formatting, both for VSCode and Phabricator;
|
changeset |
files
|
| Mon, 25 Mar 2024 17:10:19 +0100 |
wenzelm |
just one README.md;
|
changeset |
files
|
| Mon, 25 Mar 2024 17:55:02 +0100 |
nipkow |
tuned
|
changeset |
files
|
| Mon, 25 Mar 2024 15:11:48 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Mon, 25 Mar 2024 15:11:21 +0100 |
wenzelm |
more accurate platform directories: pkg/tool structure is hardwired in "go";
|
changeset |
files
|
| Mon, 25 Mar 2024 14:47:53 +0100 |
wenzelm |
support for etc/platform.props, to specify multi-platform directory structure more accurately;
|
changeset |
files
|
| Sun, 24 Mar 2024 19:14:56 +0100 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Sun, 24 Mar 2024 19:10:55 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 24 Mar 2024 19:08:13 +0100 |
wenzelm |
clarified modules;
|
changeset |
files
|
| Sun, 24 Mar 2024 18:45:40 +0100 |
wenzelm |
clarified modules;
|
changeset |
files
|
| Sun, 24 Mar 2024 17:49:53 +0100 |
wenzelm |
build Isabelle component for Go: all platforms;
|
changeset |
files
|
| Sun, 24 Mar 2024 15:13:35 +0100 |
wenzelm |
misc tuning;
|
changeset |
files
|
| Sun, 24 Mar 2024 15:05:22 +0100 |
wenzelm |
just one copy of darwin-universal.tar.gz;
|
changeset |
files
|
| Mon, 25 Mar 2024 14:08:25 +0100 |
nipkow |
documented running time function framework by Jonas Stahl
|
changeset |
files
|
| Mon, 25 Mar 2024 10:16:14 +0100 |
desharna |
merged
|
changeset |
files
|
| Sat, 23 Mar 2024 18:55:38 +0100 |
desharna |
redefined wf as an abbreviation for "wf_on UNIV"
|
changeset |
files
|
| Sun, 24 Mar 2024 14:51:03 +0100 |
nipkow |
merged
|
changeset |
files
|
| Sun, 24 Mar 2024 14:50:47 +0100 |
nipkow |
more uniform command names
|
changeset |
files
|
| Sun, 24 Mar 2024 14:15:10 +0100 |
nipkow |
tuned parameter order
|
changeset |
files
|
| Sun, 24 Mar 2024 14:04:30 +0100 |
wenzelm |
shutdown lrzcloud2;
|
changeset |
files
|
| Sat, 23 Mar 2024 07:59:53 +0100 |
desharna |
tuned NEWS
|
changeset |
files
|
| Thu, 21 Mar 2024 11:24:03 +0100 |
desharna |
redefined wfP as an abbreviation for "wfp_on UNIV"
|
changeset |
files
|
| Fri, 22 Mar 2024 10:38:35 +0100 |
desharna |
merged
|
changeset |
files
|
| Wed, 20 Mar 2024 21:13:49 +0100 |
desharna |
added lemma wellorder.wfp_on_less[simp]
|
changeset |
files
|
| Thu, 21 Mar 2024 21:04:49 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Thu, 21 Mar 2024 21:03:06 +0100 |
wenzelm |
suppress arm64-darwin, which does not support "-codegen native" (required for AFP/PAC_Checker);
|
changeset |
files
|
| Thu, 21 Mar 2024 16:54:53 +0100 |
wenzelm |
update to sumatra_pdf-3.5.2;
|
changeset |
files
|
| Thu, 21 Mar 2024 16:28:43 +0100 |
wenzelm |
tuned signature: fewer warnings in IntelliJ IDEA;
|
changeset |
files
|
| Thu, 21 Mar 2024 16:16:03 +0100 |
wenzelm |
update to jsoup-1.17.2;
|
changeset |
files
|
| Thu, 21 Mar 2024 16:15:25 +0100 |
wenzelm |
proper bib entries (amending 82aaa0d8fc3b);
|
changeset |
files
|
| Thu, 21 Mar 2024 15:00:22 +0100 |
wenzelm |
update to dotnet-8.0.203;
|
changeset |
files
|
| Thu, 21 Mar 2024 14:45:15 +0100 |
wenzelm |
enforce rebuild of Isabelle/ML;
|
changeset |
files
|
| Thu, 21 Mar 2024 14:43:40 +0100 |
wenzelm |
update to sqlite-3.45.2.0: clarified component name, following postgresql;
|
changeset |
files
|
| Thu, 21 Mar 2024 14:29:01 +0100 |
wenzelm |
activate postgresql-42.7.3;
|
changeset |
files
|
| Thu, 21 Mar 2024 14:26:45 +0100 |
wenzelm |
update to postgresql-42.7.3;
|
changeset |
files
|
| Thu, 21 Mar 2024 14:19:05 +0100 |
wenzelm |
update to mlton-20210117-2, which covers x86_64-linux, x86_64-darwin, arm64-darwin;
|
changeset |
files
|
| Thu, 21 Mar 2024 12:47:51 +0100 |
wenzelm |
isabelle update -u cite;
|
changeset |
files
|
| Thu, 21 Mar 2024 17:36:50 +0100 |
Fabian Huch |
raise error if benchmarking fails;
|
changeset |
files
|
| Thu, 21 Mar 2024 16:35:55 +0100 |
Fabian Huch |
option for benchmark session;
|
changeset |
files
|
| Thu, 21 Mar 2024 13:05:49 +0100 |
Fabian Huch |
add hosts option to run benchmark on the cluster from the command-line;
|
changeset |
files
|
| Wed, 20 Mar 2024 14:56:16 +0100 |
Fabian Huch |
only start jobs early if they are due (cf. 1966578feff8);
|
changeset |
files
|
| Thu, 21 Mar 2024 14:19:39 +0000 |
paulson |
New material from a variety of sources (including AFP)
|
changeset |
files
|
| Wed, 20 Mar 2024 21:12:49 +0100 |
wenzelm |
build component for cvc5-latest (ef2bc3f735df);
|
changeset |
files
|
| Wed, 20 Mar 2024 20:45:36 +0100 |
desharna |
merged
|
changeset |
files
|
| Wed, 20 Mar 2024 12:26:52 +0100 |
desharna |
try proof method "order" in Sledgehammer's proof reconstruction
|
changeset |
files
|
| Wed, 20 Mar 2024 11:55:58 +0100 |
desharna |
added Mirabelle action "order"
|
changeset |
files
|
| Wed, 20 Mar 2024 11:11:04 +0100 |
desharna |
renamed lemma antisymp_on_reflcp to antisymp_on_reflclp
|
changeset |
files
|
| Wed, 20 Mar 2024 09:57:14 +0100 |
desharna |
tuned proof
|
changeset |
files
|
| Wed, 20 Mar 2024 09:26:25 +0100 |
desharna |
added lemma order_reflclp_if_transp_and_asymp
|
changeset |
files
|
| Wed, 20 Mar 2024 09:24:12 +0100 |
desharna |
added lemmas antisym_on_reflcl_if_asym_on and antisymp_on_reflclp_if_asymp_on
|
changeset |
files
|
| Wed, 20 Mar 2024 17:30:44 +0100 |
Manuel Eberl |
HOL-Library: added modulo/congruence for real numbers
|
changeset |
files
|
| Wed, 20 Mar 2024 15:19:20 +0100 |
Fabian Huch |
only print schedule if relevant;
|
changeset |
files
|
| Wed, 20 Mar 2024 16:23:26 +0100 |
Fabian Huch |
remove laziness: no need, and errors during initialization loop with close();
|
changeset |
files
|
| Wed, 20 Mar 2024 16:05:15 +0100 |
Manuel Eberl |
more general definition of meromorphicity; Weierstraß factorisation theorem
|
changeset |
files
|
| Wed, 20 Mar 2024 14:05:15 +0100 |
Fabian Huch |
always provide build_database_server option in benchmark command;
|
changeset |
files
|
| Wed, 20 Mar 2024 13:58:55 +0100 |
Fabian Huch |
always check if node is defined, e.g. for exists_next operation wit empty schedule;
|
changeset |
files
|
| Tue, 19 Mar 2024 13:24:22 +0100 |
blanchet |
fixed typo
|
changeset |
files
|
| Tue, 19 Mar 2024 00:42:09 +0100 |
Fabian Huch |
disable taskset for now: performance impact is negative;
|
changeset |
files
|
| Sun, 17 Mar 2024 22:48:44 +0100 |
Fabian Huch |
allow specifying initial schedule;
|
changeset |
files
|
| Sun, 17 Mar 2024 21:55:58 +0100 |
Fabian Huch |
clarify use of num_threads vs. max_cpus;
|
changeset |
files
|
| Sun, 17 Mar 2024 21:04:00 +0100 |
Fabian Huch |
clarified host: pre-load max threads;
|
changeset |
files
|
| Sun, 17 Mar 2024 19:53:31 +0100 |
Fabian Huch |
clarified: more operations;
|
changeset |
files
|
| Sun, 17 Mar 2024 19:45:07 +0100 |
desharna |
added alias wfp for wfP
|
changeset |
files
|
| Sun, 17 Mar 2024 19:30:34 +0100 |
desharna |
merged
|
changeset |
files
|
| Sun, 17 Mar 2024 12:34:11 +0100 |
desharna |
added lemmas wf_on_antimono, wf_on_antimono_strong, wfp_on_antimono, wfp_on_antimono_strong, wf_on_subset, and wfp_on_subset
|
changeset |
files
|
| Sun, 17 Mar 2024 15:03:12 +0100 |
Fabian Huch |
start scheduled jobs earlier, if possible;
|
changeset |
files
|
| Sun, 17 Mar 2024 09:05:44 +0100 |
desharna |
tuned proofs
|
changeset |
files
|
| Sun, 17 Mar 2024 09:03:18 +0100 |
desharna |
added lemmas wfP_iff_ex_minimal, wf_iff_ex_minimal, wf_onE_pf, wf_onI_pf, wf_on_iff_ex_minimal, and wfp_on_iff_ex_minimal
|
changeset |
files
|
| Sun, 17 Mar 2024 07:45:12 +0100 |
desharna |
merged
|
changeset |
files
|
| Sat, 16 Mar 2024 09:05:17 +0100 |
desharna |
added definitions wf_on and wfp_on as restricted versions of wf and wfP respectively
|
changeset |
files
|
| Sat, 16 Mar 2024 21:22:02 +0100 |
Fabian Huch |
read/write proper schedule date (amending 9da3019e1ee5);
|
changeset |
files
|
| Sat, 16 Mar 2024 17:00:13 +0100 |
Fabian Huch |
allow read/write of schedule in build (read via option, write from tool);
|
changeset |
files
|
| Sat, 16 Mar 2024 16:46:52 +0100 |
Fabian Huch |
file representation for schedule (e.g., for generating from external tool);
|
changeset |
files
|
| Sat, 16 Mar 2024 15:00:18 +0100 |
Fabian Huch |
proper median/mean time;
|
changeset |
files
|
| Sat, 16 Mar 2024 14:43:48 +0100 |
Fabian Huch |
remove schedule outdated limit: delay is sufficient;
|
changeset |
files
|
| Sat, 16 Mar 2024 11:00:18 +0100 |
Fabian Huch |
tuned whitespace;
|
changeset |
files
|
| Sat, 16 Mar 2024 10:56:29 +0100 |
Fabian Huch |
tie-breaking in schedule optimization to pick best schedule even when run-time is dominated by large task (e.g., session with long timeout but no data yet);
|
changeset |
files
|
| Sat, 16 Mar 2024 10:03:10 +0100 |
Fabian Huch |
tuned;
|
changeset |
files
|
| Sat, 16 Mar 2024 10:02:16 +0100 |
Fabian Huch |
remove old build before generating schedule;
|
changeset |
files
|
| Sat, 16 Mar 2024 09:58:23 +0100 |
Fabian Huch |
unused;
|
changeset |
files
|
| Fri, 15 Mar 2024 20:23:50 +0100 |
desharna |
merged
|
changeset |
files
|
| Fri, 15 Mar 2024 18:54:15 +0100 |
desharna |
added lemmas antisymp_on_image, asymp_on_image, irreflp_on_image, reflp_on_image, symp_on_image, totalp_on_image, and transp_on_image
|
changeset |
files
|
| Fri, 15 Mar 2024 19:15:04 +0100 |
wenzelm |
clarified names;
|
changeset |
files
|
| Mon, 11 Mar 2024 21:46:31 +0100 |
Simon Wimmer |
sketch & explore: TODO comments are addressed in parent commits
|
changeset |
files
|
| Mon, 11 Mar 2024 21:11:23 +0100 |
Simon Wimmer |
sketch & explore: reduce unnecessary type constraints
|
changeset |
files
|
| Mon, 11 Mar 2024 21:20:36 +0100 |
Simon Wimmer |
sketch & explore: replace functionality of `sketch` by more useful `nxsketch` (and remove `nxsketch`)
|
changeset |
files
|
| Mon, 11 Mar 2024 21:31:18 +0100 |
Simon Wimmer |
sketch & explore: use Active.sendback_markup_command to preserve indentation of generated proof text
|
changeset |
files
|
| Fri, 15 Mar 2024 17:57:03 +0100 |
Fabian Huch |
change benchmark session to FOLP-ex (faster and less mean squared error than ZF-Constructible);
|
changeset |
files
|
| Thu, 14 Mar 2024 18:08:42 +0100 |
Fabian Huch |
unused;
|
changeset |
files
|
| Thu, 14 Mar 2024 17:27:40 +0100 |
Fabian Huch |
tuned;
|
changeset |
files
|
| Thu, 14 Mar 2024 17:19:01 +0100 |
Fabian Huch |
proper IPC for scheduled builds, following 7ae25372ab04;
|
changeset |
files
|
| Thu, 14 Mar 2024 15:46:39 +0100 |
Fabian Huch |
proper check (amending 9aef1d1535ff);
|
changeset |
files
|
| Thu, 14 Mar 2024 14:20:44 +0100 |
Fabian Huch |
more synced options (following 6e5397fcc41b);
|
changeset |
files
|
| Thu, 14 Mar 2024 08:24:48 +0000 |
haftmann |
avoid [no_atp] declations shadowing propositions from sledgehammer
|
changeset |
files
|
| Thu, 14 Mar 2024 10:01:51 +0100 |
Fabian Huch |
track start in build job results (following 9d484c5d3a63), so it can directly be written to build log database;
|
changeset |
files
|
| Thu, 14 Mar 2024 09:36:11 +0100 |
Fabian Huch |
use inherited build_start, following d9fc2cc37694;
|
changeset |
files
|
| Thu, 14 Mar 2024 11:03:23 +0100 |
wenzelm |
update NEWS + CONTRIBUTORS for release;
|
changeset |
files
|
| Wed, 13 Mar 2024 18:39:41 +0000 |
haftmann |
Tuned proofs
|
changeset |
files
|
| Wed, 13 Mar 2024 23:27:44 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 13 Mar 2024 23:26:30 +0100 |
wenzelm |
revert most parts of 0e79fa88cab6: somewhat ambitious attempt to move towards "editing" builds via added/canceled workers;
|
changeset |
files
|