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;