Thu, 07 Nov 2024 20:08:50 +0100 clarified signature;
wenzelm [Thu, 07 Nov 2024 20:08:50 +0100] rev 81394
clarified signature;
Thu, 07 Nov 2024 20:02:10 +0100 clarified signature;
wenzelm [Thu, 07 Nov 2024 20:02:10 +0100] rev 81393
clarified signature;
Thu, 07 Nov 2024 16:13:58 +0100 clarified output representation: postpone Pretty.separate;
wenzelm [Thu, 07 Nov 2024 16:13:58 +0100] rev 81392
clarified output representation: postpone Pretty.separate;
Thu, 07 Nov 2024 16:03:53 +0100 tuned;
wenzelm [Thu, 07 Nov 2024 16:03:53 +0100] rev 81391
tuned;
Thu, 07 Nov 2024 15:42:35 +0100 tuned: fewer warnings in IntelliJ IDEA;
wenzelm [Thu, 07 Nov 2024 15:42:35 +0100] rev 81390
tuned: fewer warnings in IntelliJ IDEA;
Thu, 07 Nov 2024 13:30:40 +0100 clarified signature: more accurate types;
wenzelm [Thu, 07 Nov 2024 13:30:40 +0100] rev 81389
clarified signature: more accurate types;
Thu, 07 Nov 2024 13:26:31 +0100 tuned signature: more standard names;
wenzelm [Thu, 07 Nov 2024 13:26:31 +0100] rev 81388
tuned signature: more standard names;
Thu, 07 Nov 2024 13:22:59 +0100 more uniform pretty_text_area.zoom via its zoom_component;
wenzelm [Thu, 07 Nov 2024 13:22:59 +0100] rev 81387
more uniform pretty_text_area.zoom via its zoom_component;
Thu, 07 Nov 2024 12:35:55 +0100 tuned signature;
wenzelm [Thu, 07 Nov 2024 12:35:55 +0100] rev 81386
tuned signature;
Thu, 07 Nov 2024 12:32:44 +0100 tuned signature: more standard names;
wenzelm [Thu, 07 Nov 2024 12:32:44 +0100] rev 81385
tuned signature: more standard names;
Thu, 07 Nov 2024 12:26:36 +0100 tuned;
wenzelm [Thu, 07 Nov 2024 12:26:36 +0100] rev 81384
tuned;
Thu, 07 Nov 2024 12:17:18 +0100 clarified signature;
wenzelm [Thu, 07 Nov 2024 12:17:18 +0100] rev 81383
clarified signature;
Thu, 07 Nov 2024 12:08:32 +0100 clarified signature;
wenzelm [Thu, 07 Nov 2024 12:08:32 +0100] rev 81382
clarified signature;
Thu, 07 Nov 2024 11:46:21 +0100 tuned;
wenzelm [Thu, 07 Nov 2024 11:46:21 +0100] rev 81381
tuned;
Thu, 07 Nov 2024 11:35:39 +0100 revert 1206400b9b48: proper Node.unapply for Node.apply(null);
wenzelm [Thu, 07 Nov 2024 11:35:39 +0100] rev 81380
revert 1206400b9b48: proper Node.unapply for Node.apply(null);
Wed, 06 Nov 2024 22:04:05 +0100 tuned signature;
wenzelm [Wed, 06 Nov 2024 22:04:05 +0100] rev 81379
tuned signature;
Wed, 06 Nov 2024 16:07:30 +0100 clarified signature;
wenzelm [Wed, 06 Nov 2024 16:07:30 +0100] rev 81378
clarified signature;
Wed, 06 Nov 2024 15:52:31 +0100 clarified signature, with subtle change of semantics: proper non-null result;
wenzelm [Wed, 06 Nov 2024 15:52:31 +0100] rev 81377
clarified signature, with subtle change of semantics: proper non-null result;
Wed, 06 Nov 2024 15:38:45 +0100 clarified modules;
wenzelm [Wed, 06 Nov 2024 15:38:45 +0100] rev 81376
clarified modules;
Wed, 06 Nov 2024 15:17:39 +0100 more robust and uniform metric, still with special treatment motivated by jEdit (see also 0cdfce0bf956);
wenzelm [Wed, 06 Nov 2024 15:17:39 +0100] rev 81375
more robust and uniform metric, still with special treatment motivated by jEdit (see also 0cdfce0bf956);
Wed, 06 Nov 2024 11:05:18 +0100 misc tuning;
wenzelm [Wed, 06 Nov 2024 11:05:18 +0100] rev 81374
misc tuning;
Fri, 08 Nov 2024 18:13:55 +0100 try0: avoid mapping background theory -- should be handled by Context_Position visibility;
Fabian Huch <huch@in.tum.de> [Fri, 08 Nov 2024 18:13:55 +0100] rev 81373
try0: avoid mapping background theory -- should be handled by Context_Position visibility;
Thu, 31 Oct 2024 11:35:24 +0100 try0: stop early if more subgoals are created;
Fabian Huch <huch@in.tum.de> [Thu, 31 Oct 2024 11:35:24 +0100] rev 81372
try0: stop early if more subgoals are created;
Fri, 25 Oct 2024 16:38:15 +0200 try0: filter out untagged thms;
Fabian Huch <huch@in.tum.de> [Fri, 25 Oct 2024 16:38:15 +0200] rev 81371
try0: filter out untagged thms;
Thu, 24 Oct 2024 19:13:49 +0200 try0: support literal facts;
Fabian Huch <huch@in.tum.de> [Thu, 24 Oct 2024 19:13:49 +0200] rev 81370
try0: support literal facts;
Thu, 24 Oct 2024 16:46:25 +0200 try0: add 'use' modifier for thms to insert;
Fabian Huch <huch@in.tum.de> [Thu, 24 Oct 2024 16:46:25 +0200] rev 81369
try0: add 'use' modifier for thms to insert;
Thu, 24 Oct 2024 16:45:09 +0200 try0: use extra thms via insert;
Fabian Huch <huch@in.tum.de> [Thu, 24 Oct 2024 16:45:09 +0200] rev 81368
try0: use extra thms via insert;
Thu, 24 Oct 2024 18:25:17 +0200 clarified: proper type for facts;
Fabian Huch <huch@in.tum.de> [Thu, 24 Oct 2024 18:25:17 +0200] rev 81367
clarified: proper type for facts;
Thu, 24 Oct 2024 18:16:36 +0200 clarified: proper type;
Fabian Huch <huch@in.tum.de> [Thu, 24 Oct 2024 18:16:36 +0200] rev 81366
clarified: proper type;
Thu, 24 Oct 2024 14:08:28 +0200 tuned;
Fabian Huch <huch@in.tum.de> [Thu, 24 Oct 2024 14:08:28 +0200] rev 81365
tuned;
Thu, 24 Oct 2024 14:07:13 +0200 tuned;
Fabian Huch <huch@in.tum.de> [Thu, 24 Oct 2024 14:07:13 +0200] rev 81364
tuned;
Thu, 24 Oct 2024 11:37:41 +0200 try0: pass tagged thms for better control;
Fabian Huch <huch@in.tum.de> [Thu, 24 Oct 2024 11:37:41 +0200] rev 81363
try0: pass tagged thms for better control;
Tue, 22 Oct 2024 17:31:54 +0200 clarified: proper return type;
Fabian Huch <huch@in.tum.de> [Tue, 22 Oct 2024 17:31:54 +0200] rev 81362
clarified: proper return type;
Tue, 22 Oct 2024 14:34:13 +0200 improve try0: solve multiple subgoals at once, if possible;
Fabian Huch <huch@in.tum.de> [Tue, 22 Oct 2024 14:34:13 +0200] rev 81361
improve try0: solve multiple subgoals at once, if possible;
Tue, 22 Oct 2024 14:31:25 +0200 tuned: unused parameter;
Fabian Huch <huch@in.tum.de> [Tue, 22 Oct 2024 14:31:25 +0200] rev 81360
tuned: unused parameter;
Fri, 08 Nov 2024 11:18:08 +0100 tuned
nipkow [Fri, 08 Nov 2024 11:18:08 +0100] rev 81359
tuned
Thu, 07 Nov 2024 16:21:57 +0100 better termination behaviour
nipkow [Thu, 07 Nov 2024 16:21:57 +0100] rev 81358
better termination behaviour
Wed, 06 Nov 2024 18:10:39 +0100 uniform name T_f for closed-form lemmas for function T_f
nipkow [Wed, 06 Nov 2024 18:10:39 +0100] rev 81357
uniform name T_f for closed-form lemmas for function T_f
Wed, 06 Nov 2024 16:27:06 +0100 More time for primitive functions
nipkow [Wed, 06 Nov 2024 16:27:06 +0100] rev 81356
More time for primitive functions
Wed, 06 Nov 2024 16:19:45 +0100 merged Reverse into Time_Funs
nipkow [Wed, 06 Nov 2024 16:19:45 +0100] rev 81355
merged Reverse into Time_Funs
Tue, 05 Nov 2024 23:51:44 +0100 tuned proofs;
wenzelm [Tue, 05 Nov 2024 23:51:44 +0100] rev 81354
tuned proofs;
Tue, 05 Nov 2024 23:45:39 +0100 tuned description: plain text documentation is also supported;
wenzelm [Tue, 05 Nov 2024 23:45:39 +0100] rev 81353
tuned description: plain text documentation is also supported;
Tue, 05 Nov 2024 23:27:47 +0100 merged
wenzelm [Tue, 05 Nov 2024 23:27:47 +0100] rev 81352
merged
Tue, 05 Nov 2024 23:01:09 +0100 update to jdk-21.0.5;
wenzelm [Tue, 05 Nov 2024 23:01:09 +0100] rev 81351
update to jdk-21.0.5; enforce rebuild of Isabelle/ML and Isabelle/Scala;
Tue, 05 Nov 2024 22:05:50 +0100 misc tuning and clarification: Doc.Entry supports both plain files and pdf documents;
wenzelm [Tue, 05 Nov 2024 22:05:50 +0100] rev 81350
misc tuning and clarification: Doc.Entry supports both plain files and pdf documents; recover plain file support from 488c7e8923b2;
Tue, 05 Nov 2024 19:59:30 +0100 tuned proofs
nipkow [Tue, 05 Nov 2024 19:59:30 +0100] rev 81349
tuned proofs
Tue, 05 Nov 2024 19:52:15 +0100 added missing definitions
nipkow [Tue, 05 Nov 2024 19:52:15 +0100] rev 81348
added missing definitions
Mon, 04 Nov 2024 22:36:42 +0100 tuned proofs;
wenzelm [Mon, 04 Nov 2024 22:36:42 +0100] rev 81347
tuned proofs; more Isabelle symbols;
Mon, 04 Nov 2024 22:05:20 +0100 clarified modules;
wenzelm [Mon, 04 Nov 2024 22:05:20 +0100] rev 81346
clarified modules;
Mon, 04 Nov 2024 21:54:34 +0100 support value-oriented Font_Metric, e.g. for caching Pretty output;
wenzelm [Mon, 04 Nov 2024 21:54:34 +0100] rev 81345
support value-oriented Font_Metric, e.g. for caching Pretty output;
Mon, 04 Nov 2024 21:25:26 +0100 tuned;
wenzelm [Mon, 04 Nov 2024 21:25:26 +0100] rev 81344
tuned;
Mon, 04 Nov 2024 21:05:11 +0100 unused;
wenzelm [Mon, 04 Nov 2024 21:05:11 +0100] rev 81343
unused;
Mon, 04 Nov 2024 21:05:05 +0100 tuned;
wenzelm [Mon, 04 Nov 2024 21:05:05 +0100] rev 81342
tuned;
Mon, 04 Nov 2024 21:00:31 +0100 tuned;
wenzelm [Mon, 04 Nov 2024 21:00:31 +0100] rev 81341
tuned;
Mon, 04 Nov 2024 20:55:01 +0100 clarified signature;
wenzelm [Mon, 04 Nov 2024 20:55:01 +0100] rev 81340
clarified signature; clarified modules;
Mon, 04 Nov 2024 14:50:21 +0100 more accurate Symbol.Metric, following 6eccae338770;
wenzelm [Mon, 04 Nov 2024 14:50:21 +0100] rev 81339
more accurate Symbol.Metric, following 6eccae338770;
Mon, 04 Nov 2024 14:39:27 +0100 tuned rendering, notably for HiDPI on Linux (see also ca7e2c21b104);
wenzelm [Mon, 04 Nov 2024 14:39:27 +0100] rev 81338
tuned rendering, notably for HiDPI on Linux (see also ca7e2c21b104);
Mon, 04 Nov 2024 14:10:21 +0100 proper parentheses, for the sake of IntelliJ IDEA;
wenzelm [Mon, 04 Nov 2024 14:10:21 +0100] rev 81337
proper parentheses, for the sake of IntelliJ IDEA;
Mon, 04 Nov 2024 12:58:05 +0100 clarified modules;
wenzelm [Mon, 04 Nov 2024 12:58:05 +0100] rev 81336
clarified modules;
Mon, 04 Nov 2024 12:22:24 +0100 clarified signature;
wenzelm [Mon, 04 Nov 2024 12:22:24 +0100] rev 81335
clarified signature;
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 tip