| Thu, 05 Jan 2023 21:33:49 +0100 |
wenzelm |
isabelle update -u path_cartouches;
|
changeset |
files
|
| Thu, 05 Jan 2023 21:18:55 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Thu, 05 Jan 2023 21:14:53 +0100 |
wenzelm |
updated documentation;
|
changeset |
files
|
| Thu, 05 Jan 2023 21:14:37 +0100 |
wenzelm |
more options;
|
changeset |
files
|
| Thu, 05 Jan 2023 20:44:10 +0100 |
wenzelm |
tuned message;
|
changeset |
files
|
| Thu, 05 Jan 2023 20:25:41 +0100 |
wenzelm |
isabelle update no longer uses PIDE dump, but regular session build database: more scalable;
|
changeset |
files
|
| Thu, 05 Jan 2023 20:13:04 +0100 |
wenzelm |
more robust;
|
changeset |
files
|
| Thu, 05 Jan 2023 20:07:22 +0100 |
wenzelm |
more operations;
|
changeset |
files
|
| Thu, 05 Jan 2023 19:41:12 +0100 |
wenzelm |
proper Node.init_blobs, not just edits (amending ca872f20cf5b);
|
changeset |
files
|
| Thu, 05 Jan 2023 17:14:29 +0100 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Thu, 05 Jan 2023 17:00:22 +0100 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Thu, 05 Jan 2023 16:44:15 +0100 |
wenzelm |
clarified session sources: theory and blobs are read from database, instead of physical file-system;
|
changeset |
files
|
| Thu, 05 Jan 2023 12:43:05 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 04 Jan 2023 16:40:02 +0100 |
wenzelm |
clarified signature: more operations;
|
changeset |
files
|
| Wed, 04 Jan 2023 16:06:46 +0100 |
wenzelm |
clarified signature: more operations;
|
changeset |
files
|
| Wed, 04 Jan 2023 15:53:36 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 04 Jan 2023 15:42:00 +0100 |
wenzelm |
more direct access to session_sources, without somewhat fragile file-system operations;
|
changeset |
files
|
| Wed, 04 Jan 2023 15:02:48 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 04 Jan 2023 14:56:22 +0100 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Wed, 04 Jan 2023 14:50:11 +0100 |
wenzelm |
tuned signature: avoid confusion with Document.Node.Blob and Command.Blob;
|
changeset |
files
|
| Wed, 04 Jan 2023 14:35:19 +0100 |
wenzelm |
clarified signature: old node is ignored;
|
changeset |
files
|
| Wed, 04 Jan 2023 14:26:30 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 04 Jan 2023 13:39:40 +0100 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Wed, 04 Jan 2023 19:06:16 +0000 |
paulson |
final tidying of theorems
|
changeset |
files
|
| Wed, 04 Jan 2023 17:46:27 +0000 |
paulson |
merged
|
changeset |
files
|
| Wed, 04 Jan 2023 10:27:32 +0000 |
paulson |
merged
|
changeset |
files
|
| Wed, 04 Jan 2023 10:27:19 +0000 |
paulson |
continued proof simplification
|
changeset |
files
|
| Tue, 03 Jan 2023 19:55:35 +0000 |
paulson |
merged
|
changeset |
files
|
| Tue, 03 Jan 2023 19:55:24 +0000 |
paulson |
Further simplifications
|
changeset |
files
|
| Tue, 03 Jan 2023 17:02:41 +0000 |
paulson |
More tidying of proofs
|
changeset |
files
|
| Wed, 04 Jan 2023 13:21:45 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 03 Jan 2023 21:22:24 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Tue, 03 Jan 2023 21:22:04 +0100 |
wenzelm |
discontinued fragile operation;
|
changeset |
files
|
| Tue, 03 Jan 2023 21:18:15 +0100 |
wenzelm |
more robust operations: avoid somewhat fragile Document.Node.Name.master_dir_path;
|
changeset |
files
|
| Tue, 03 Jan 2023 20:46:56 +0100 |
wenzelm |
tuned whitespace;
|
changeset |
files
|
| Tue, 03 Jan 2023 20:34:51 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 03 Jan 2023 17:21:24 +0100 |
wenzelm |
avoid somewhat fragile Document.Node.Name.master_dir_path;
|
changeset |
files
|
| Tue, 03 Jan 2023 16:53:43 +0100 |
wenzelm |
clarified signature: avoid somewhat fragile Document.Node.Name.master_dir_path;
|
changeset |
files
|
| Tue, 03 Jan 2023 16:14:17 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 03 Jan 2023 16:05:07 +0100 |
wenzelm |
clarified modules;
|
changeset |
files
|
| Tue, 03 Jan 2023 15:42:25 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 03 Jan 2023 15:32:54 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 03 Jan 2023 15:03:48 +0100 |
wenzelm |
clarified master_dir: avoid somewhat fragile Document.Node.Name.master_dir_path;
|
changeset |
files
|
| Tue, 03 Jan 2023 14:00:59 +0100 |
wenzelm |
tuned signature: avoid too many aliases (see also 72daee8a39ca);
|
changeset |
files
|
| Tue, 03 Jan 2023 12:58:00 +0100 |
wenzelm |
clarified modules;
|
changeset |
files
|
| Tue, 03 Jan 2023 18:23:52 +0100 |
desharna |
merged
|
changeset |
files
|
| Mon, 26 Dec 2022 14:34:32 +0100 |
desharna |
strengthened and renamed lemmas asym_on_iff_irrefl_on_if_trans and asymp_on_iff_irreflp_on_if_transp
|
changeset |
files
|
| Tue, 03 Jan 2023 11:30:37 +0000 |
paulson |
Fixed a couple of simple_path occurrences
|
changeset |
files
|
| Mon, 02 Jan 2023 20:47:09 +0000 |
paulson |
merged
|
changeset |
files
|
| Mon, 02 Jan 2023 20:46:24 +0000 |
paulson |
Tidying up of paths, introducing "loop_free" as a separate predicate in the definition of "simple_path"
|
changeset |
files
|
| Mon, 02 Jan 2023 20:39:21 +0100 |
wenzelm |
clarified signature: more explicit types;
|
changeset |
files
|
| Mon, 02 Jan 2023 20:24:43 +0100 |
wenzelm |
more robust: prefer internal theory names;
|
changeset |
files
|
| Mon, 02 Jan 2023 16:02:16 +0100 |
wenzelm |
clarified session_sources (again, see also 9d0e6ea7aa68);
|
changeset |
files
|
| Mon, 02 Jan 2023 15:41:50 +0100 |
wenzelm |
clarified signature: more explicit types;
|
changeset |
files
|
| Mon, 02 Jan 2023 15:30:57 +0100 |
wenzelm |
tuned output;
|
changeset |
files
|
| Mon, 02 Jan 2023 15:28:33 +0100 |
wenzelm |
clarified signature: more general operations;
|
changeset |
files
|
| Mon, 02 Jan 2023 15:18:13 +0100 |
wenzelm |
clarified signature: more explicit types;
|
changeset |
files
|
| Mon, 02 Jan 2023 15:05:15 +0100 |
wenzelm |
clarified signature: more explicit types (see also 90c552d28d36);
|
changeset |
files
|
| Mon, 02 Jan 2023 13:54:40 +0100 |
wenzelm |
do write_session_sources early, to have information available in build job;
|
changeset |
files
|
| Mon, 02 Jan 2023 13:09:38 +0100 |
wenzelm |
tuned signature, following Url.append_path;
|
changeset |
files
|