wenzelm [Sat, 02 Nov 2024 15:22:50 +0100] rev 81310
clarified signature;
wenzelm [Sat, 02 Nov 2024 14:58:50 +0100] rev 81309
clarified modules: more re-usable;
wenzelm [Sat, 02 Nov 2024 14:56:13 +0100] rev 81308
proper protocol messages (amending 7a1f9e571046);
wenzelm [Fri, 01 Nov 2024 19:20:52 +0100] rev 81307
clarified treatment of caret_range: better support for multiple (unrelated) selections;
wenzelm [Fri, 01 Nov 2024 19:11:40 +0100] rev 81306
tuned whitespace;
wenzelm [Fri, 01 Nov 2024 18:55:47 +0100] rev 81305
support incremental isabelle.select-structure --- like select-block, but based on selection instead of caret;
wenzelm [Fri, 01 Nov 2024 18:17:03 +0100] rev 81304
clarified rendering: entity acts as atomic notation / expression;
wenzelm [Fri, 01 Nov 2024 18:12:40 +0100] rev 81303
more rendering for Markup.COMMAND_SPAN, following Rendering.structure_elements;
wenzelm [Fri, 01 Nov 2024 17:13:42 +0100] rev 81302
more NEWS;
wenzelm [Fri, 01 Nov 2024 16:57:33 +0100] rev 81301
merged
wenzelm [Fri, 01 Nov 2024 16:53:10 +0100] rev 81300
support Isabelle/jEdit action isabelle.select_structure;
update component jedit-20241101;
wenzelm [Fri, 01 Nov 2024 15:40:31 +0100] rev 81299
more operations;
wenzelm [Tue, 29 Oct 2024 21:51:21 +0100] rev 81298
clarified text;
wenzelm [Tue, 29 Oct 2024 12:30:15 +0100] rev 81297
update to jedit5.7.0;
wenzelm [Mon, 28 Oct 2024 09:43:28 +0100] rev 81296
GUI option "editor_auto_hovering" for Output panel;
wenzelm [Mon, 28 Oct 2024 09:40:28 +0100] rev 81295
update to scala-3.3.4 LTS;
wenzelm [Mon, 28 Oct 2024 08:48:31 +0100] rev 81294
removed obsolete markup for "open_block" (see also d5ad89fda714): Isabelle/Scala directly supports XML.Elem pretty-printing;
paulson <lp15@cam.ac.uk> [Fri, 01 Nov 2024 14:10:52 +0000] rev 81293
Library material from Eberl's Parallel_Shear_Sort
paulson <lp15@cam.ac.uk> [Fri, 01 Nov 2024 12:15:53 +0000] rev 81292
Trying to clean up these horribly ugly old proofs, but the requirement of constructivity makes it very difficult
Manuel Eberl <manuel@pruvisto.org> [Thu, 31 Oct 2024 18:43:32 +0100] rev 81291
use automatically generated time function in HOL-Data_Structures.Selection
nipkow [Thu, 31 Oct 2024 15:46:53 +0100] rev 81290
merged
nipkow [Thu, 31 Oct 2024 15:46:33 +0100] rev 81289
better time_functions (let)
Fabian Huch <huch@in.tum.de> [Thu, 31 Oct 2024 14:58:53 +0100] rev 81288
less hidden configuration;
Fabian Huch <huch@in.tum.de> [Thu, 31 Oct 2024 14:56:59 +0100] rev 81287
proper passwordless smtp check: must be null;
blanchet [Thu, 31 Oct 2024 09:24:10 +0100] rev 81286
adjusted documentation
nipkow [Tue, 29 Oct 2024 10:26:06 +0100] rev 81285
more attribute tuning
nipkow [Tue, 29 Oct 2024 07:41:52 +0100] rev 81284
tuned attributes
nipkow [Mon, 28 Oct 2024 18:48:28 +0100] rev 81283
merged
nipkow [Mon, 28 Oct 2024 18:48:14 +0100] rev 81282
added lemmas
wenzelm [Sun, 27 Oct 2024 22:35:02 +0100] rev 81281
tuned proofs;
wenzelm [Sun, 27 Oct 2024 20:11:08 +0100] rev 81280
tuned NEWS;
wenzelm [Sun, 27 Oct 2024 19:57:29 +0100] rev 81279
markup for "..." notation;
clarified signature;
wenzelm [Sun, 27 Oct 2024 15:30:00 +0100] rev 81278
more robust: avoid non-authentic translations;
wenzelm [Sun, 27 Oct 2024 12:54:58 +0100] rev 81277
tuned whitespace of sources;
wenzelm [Sun, 27 Oct 2024 12:47:27 +0100] rev 81276
update documentation;
tuned typesetting;
wenzelm [Sun, 27 Oct 2024 12:32:40 +0100] rev 81275
tuned;
wenzelm [Sun, 27 Oct 2024 12:23:48 +0100] rev 81274
update documentation: print mode "latex" only affects syntax tables, but output of symbols;
wenzelm [Sun, 27 Oct 2024 12:13:34 +0100] rev 81273
misc tuning and clarification;
wenzelm [Sun, 27 Oct 2024 11:48:32 +0100] rev 81272
clarified section structure;
wenzelm [Sun, 27 Oct 2024 11:46:04 +0100] rev 81271
tuned;
wenzelm [Sun, 27 Oct 2024 11:34:51 +0100] rev 81270
tuned;
wenzelm [Sun, 27 Oct 2024 11:31:42 +0100] rev 81269
tuned;
wenzelm [Sun, 27 Oct 2024 11:22:34 +0100] rev 81268
tuned signature;
wenzelm [Sun, 27 Oct 2024 11:13:42 +0100] rev 81267
clarified symbolic output: avoid redundant "block" element for open_block = true;
wenzelm [Sun, 27 Oct 2024 11:02:21 +0100] rev 81266
clarified signature;
wenzelm [Sat, 26 Oct 2024 20:18:51 +0200] rev 81265
clarified (again): Markup.intensify is already part of Variable.markup_fixed for undeclared variable, Markup.fixed is already part of Mariable.markup;
wenzelm [Sat, 26 Oct 2024 16:07:31 +0200] rev 81264
more accurate Symbol.length;
wenzelm [Sat, 26 Oct 2024 16:07:03 +0200] rev 81263
tuned;
wenzelm [Fri, 25 Oct 2024 22:22:21 +0200] rev 81262
merged
wenzelm [Fri, 25 Oct 2024 16:03:58 +0200] rev 81261
more inner-syntax markup;
wenzelm [Fri, 25 Oct 2024 15:48:40 +0200] rev 81260
obsolete (see a8502d492dde);
wenzelm [Fri, 25 Oct 2024 15:39:27 +0200] rev 81259
minor performance tuning;
wenzelm [Fri, 25 Oct 2024 13:43:12 +0200] rev 81258
tuned proofs;
tuned whitespace;
wenzelm [Fri, 25 Oct 2024 11:31:16 +0200] rev 81257
more inner-syntax markup;
nipkow [Fri, 25 Oct 2024 17:01:23 +0200] rev 81256
merged
nipkow [Fri, 25 Oct 2024 16:57:17 +0200] rev 81255
time_fun: lambdas and lets work now
blanchet [Fri, 25 Oct 2024 15:31:58 +0200] rev 81254
variable instantiation in Sledgehammer and Metis
wenzelm [Thu, 24 Oct 2024 22:05:57 +0200] rev 81253
prefer rewrite_term_yoyo for improved performance and occasionally better results (conforming to Ast.normalize);
wenzelm [Thu, 24 Oct 2024 12:44:48 +0200] rev 81252
revert b35c2aa05fcf: redundant due to 89ea66c2045b, if object-logic judgment lacks delimiters;
wenzelm [Thu, 24 Oct 2024 12:42:41 +0200] rev 81251
clarified position constraints: omit redundant information, e.g. for implicit object-logic judgment;