wenzelm [Tue, 03 Jan 2023 21:22:24 +0100] rev 76892
merged
wenzelm [Tue, 03 Jan 2023 21:22:04 +0100] rev 76891
discontinued fragile operation;
wenzelm [Tue, 03 Jan 2023 21:18:15 +0100] rev 76890
more robust operations: avoid somewhat fragile Document.Node.Name.master_dir_path;
wenzelm [Tue, 03 Jan 2023 20:46:56 +0100] rev 76889
tuned whitespace;
wenzelm [Tue, 03 Jan 2023 20:34:51 +0100] rev 76888
tuned;
wenzelm [Tue, 03 Jan 2023 17:21:24 +0100] rev 76887
avoid somewhat fragile Document.Node.Name.master_dir_path;
wenzelm [Tue, 03 Jan 2023 16:53:43 +0100] rev 76886
clarified signature: avoid somewhat fragile Document.Node.Name.master_dir_path;
wenzelm [Tue, 03 Jan 2023 16:14:17 +0100] rev 76885
tuned;
wenzelm [Tue, 03 Jan 2023 16:05:07 +0100] rev 76884
clarified modules;
wenzelm [Tue, 03 Jan 2023 15:42:25 +0100] rev 76883
tuned;
wenzelm [Tue, 03 Jan 2023 15:32:54 +0100] rev 76882
tuned;
wenzelm [Tue, 03 Jan 2023 15:03:48 +0100] rev 76881
clarified master_dir: avoid somewhat fragile Document.Node.Name.master_dir_path;
wenzelm [Tue, 03 Jan 2023 14:00:59 +0100] rev 76880
tuned signature: avoid too many aliases (see also 72daee8a39ca);
wenzelm [Tue, 03 Jan 2023 12:58:00 +0100] rev 76879
clarified modules;
desharna [Tue, 03 Jan 2023 18:23:52 +0100] rev 76878
merged
desharna [Mon, 26 Dec 2022 14:34:32 +0100] rev 76877
strengthened and renamed lemmas asym_on_iff_irrefl_on_if_trans and asymp_on_iff_irreflp_on_if_transp
paulson <lp15@cam.ac.uk> [Tue, 03 Jan 2023 11:30:37 +0000] rev 76876
Fixed a couple of simple_path occurrences
paulson [Mon, 02 Jan 2023 20:47:09 +0000] rev 76875
merged
paulson <lp15@cam.ac.uk> [Mon, 02 Jan 2023 20:46:24 +0000] rev 76874
Tidying up of paths, introducing "loop_free" as a separate predicate in the definition of "simple_path"
wenzelm [Mon, 02 Jan 2023 20:39:21 +0100] rev 76873
clarified signature: more explicit types;
wenzelm [Mon, 02 Jan 2023 20:24:43 +0100] rev 76872
more robust: prefer internal theory names;
wenzelm [Mon, 02 Jan 2023 16:02:16 +0100] rev 76871
clarified session_sources (again, see also 9d0e6ea7aa68);
wenzelm [Mon, 02 Jan 2023 15:41:50 +0100] rev 76870
clarified signature: more explicit types;
wenzelm [Mon, 02 Jan 2023 15:30:57 +0100] rev 76869
tuned output;
wenzelm [Mon, 02 Jan 2023 15:28:33 +0100] rev 76868
clarified signature: more general operations;
wenzelm [Mon, 02 Jan 2023 15:18:13 +0100] rev 76867
clarified signature: more explicit types;
wenzelm [Mon, 02 Jan 2023 15:05:15 +0100] rev 76866
clarified signature: more explicit types (see also 90c552d28d36);
wenzelm [Mon, 02 Jan 2023 13:54:40 +0100] rev 76865
do write_session_sources early, to have information available in build job;
wenzelm [Mon, 02 Jan 2023 13:09:38 +0100] rev 76864
tuned signature, following Url.append_path;
wenzelm [Mon, 02 Jan 2023 12:56:31 +0100] rev 76863
do not bundle Isabelle/Naproche, while it keeps changing;
wenzelm [Mon, 02 Jan 2023 12:45:24 +0100] rev 76862
tuned signature;
wenzelm [Mon, 02 Jan 2023 12:34:20 +0100] rev 76861
tuned;
wenzelm [Mon, 02 Jan 2023 12:29:08 +0100] rev 76860
clarified signature: uniform master_dir instead of separate field;
wenzelm [Mon, 02 Jan 2023 11:57:57 +0100] rev 76859
more standard master_dir;
wenzelm [Sun, 01 Jan 2023 22:54:40 +0100] rev 76858
tuned signature, following Url.append_path;
wenzelm [Sun, 01 Jan 2023 22:01:53 +0100] rev 76857
merged
wenzelm [Sun, 01 Jan 2023 22:01:45 +0100] rev 76856
more robust, for the sake of very rare duplicate files: src/Doc/Prog_Prove/MyList.thy and $AFP/Case_Labeling/util.ML;
wenzelm [Sun, 01 Jan 2023 21:44:08 +0100] rev 76855
store session sources within build database: timing e.g. 150ms for HOL and < 50ms for common sessions;
enforce rebuild of Isabelle/ML to update build databases;
wenzelm [Sat, 31 Dec 2022 15:48:12 +0100] rev 76854
tuned signature;
wenzelm [Sat, 31 Dec 2022 15:45:53 +0100] rev 76853
tuned;
wenzelm [Sat, 31 Dec 2022 15:42:13 +0100] rev 76852
tunes signature;
wenzelm [Sat, 31 Dec 2022 15:32:12 +0100] rev 76851
clarified signature;
wenzelm [Sat, 31 Dec 2022 14:58:34 +0100] rev 76850
tuned signature;
wenzelm [Sat, 31 Dec 2022 14:54:20 +0100] rev 76849
more systematic Sessions.illegal_theory, based on File_Format.theory_excluded;
wenzelm [Sat, 31 Dec 2022 12:38:48 +0100] rev 76848
tuned;
wenzelm [Sat, 31 Dec 2022 12:35:00 +0100] rev 76847
unused;
wenzelm [Sat, 31 Dec 2022 12:31:31 +0100] rev 76846
tuned;
wenzelm [Sat, 31 Dec 2022 12:25:34 +0100] rev 76845
clarified modules;
wenzelm [Sat, 31 Dec 2022 12:16:22 +0100] rev 76844
tuned: no need to map master_dir, which does not participate in comparison;
wenzelm [Sat, 31 Dec 2022 12:10:14 +0100] rev 76843
tuned signature;
wenzelm [Sat, 31 Dec 2022 11:58:45 +0100] rev 76842
tuned signature;
wenzelm [Sat, 31 Dec 2022 11:51:04 +0100] rev 76841
tuned comments;
wenzelm [Sat, 31 Dec 2022 11:48:32 +0100] rev 76840
clarified signature;
wenzelm [Sat, 31 Dec 2022 11:35:28 +0100] rev 76839
tuned;
paulson <lp15@cam.ac.uk> [Sun, 01 Jan 2023 12:24:00 +0000] rev 76838
removed an unfortunate sledgehammer command
paulson <lp15@cam.ac.uk> [Sun, 01 Jan 2023 01:43:02 +0000] rev 76837
A couple of patches
paulson <lp15@cam.ac.uk> [Sun, 01 Jan 2023 00:45:55 +0000] rev 76836
Big simplifications of old proofs
paulson <lp15@cam.ac.uk> [Sat, 31 Dec 2022 11:09:19 +0000] rev 76835
repaired a proof
paulson <lp15@cam.ac.uk> [Fri, 30 Dec 2022 23:21:37 +0000] rev 76834
Continued proof simplifications
paulson [Fri, 30 Dec 2022 20:59:38 +0000] rev 76833
merged