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
paulson <lp15@cam.ac.uk> [Fri, 30 Dec 2022 17:48:41 +0000] rev 76832
A further round of proof consolidation
wenzelm [Fri, 30 Dec 2022 21:27:57 +0100] rev 76831
tuned signature: avoid too many aliases;
wenzelm [Fri, 30 Dec 2022 21:09:50 +0100] rev 76830
proper thread context (amending 01a7265db76b) -- at the danger of blocking the GUI;
wenzelm [Fri, 30 Dec 2022 20:38:29 +0100] rev 76829
more robust: avoid detour via somewhat fragile Node.Name.path;
wenzelm [Fri, 30 Dec 2022 20:26:28 +0100] rev 76828
clarified generic path operations;
wenzelm [Fri, 30 Dec 2022 16:23:32 +0100] rev 76827
more flexible: implicit support for Windows;
wenzelm [Fri, 30 Dec 2022 13:25:29 +0100] rev 76826
tuned signature;
wenzelm [Fri, 30 Dec 2022 12:41:08 +0100] rev 76825
clarified output;
wenzelm [Fri, 30 Dec 2022 12:34:49 +0100] rev 76824
tuned;
paulson [Thu, 29 Dec 2022 22:14:25 +0000] rev 76823
merged
paulson <lp15@cam.ac.uk> [Thu, 29 Dec 2022 22:14:12 +0000] rev 76822
More tidying
paulson <lp15@cam.ac.uk> [Thu, 29 Dec 2022 16:32:56 +0000] rev 76821
Further cleaning up of messy proofs
paulson [Thu, 29 Dec 2022 11:46:32 +0000] rev 76820
merged
paulson <lp15@cam.ac.uk> [Thu, 29 Dec 2022 11:46:06 +0000] rev 76819
reorganisation and simplification of theorems about transcendental functions
wenzelm [Thu, 29 Dec 2022 16:44:45 +0100] rev 76818
tuned signature;
wenzelm [Thu, 29 Dec 2022 16:17:29 +0100] rev 76817
support asynchronous presentation commands, but not for "no_update" / "Keep", which is usually forked via "Toplevel.diag";
wenzelm [Thu, 29 Dec 2022 15:54:49 +0100] rev 76816
tuned whitespace;
wenzelm [Thu, 29 Dec 2022 15:39:18 +0100] rev 76815
clarified signature;
wenzelm [Thu, 29 Dec 2022 14:54:32 +0100] rev 76814
clarified signature;
wenzelm [Thu, 29 Dec 2022 13:00:16 +0100] rev 76813
tuned;
wenzelm [Thu, 29 Dec 2022 12:34:40 +0100] rev 76812
tuned;
wenzelm [Thu, 29 Dec 2022 12:27:55 +0100] rev 76811
discontinued somewhat pointless exception FAILURE with its "alt_state", which was originally due to quasi-mutable states (see 169e5b07ec06);
wenzelm [Thu, 29 Dec 2022 12:08:58 +0100] rev 76810
tuned --- more robust ML patterns;
wenzelm [Thu, 29 Dec 2022 11:49:11 +0100] rev 76809
tuned;
wenzelm [Wed, 28 Dec 2022 22:37:46 +0100] rev 76808
merged
wenzelm [Wed, 28 Dec 2022 17:39:34 +0100] rev 76807
tuned signature, for the sake of AFP/Isabelle_C;
wenzelm [Wed, 28 Dec 2022 16:49:43 +0100] rev 76806
more uniform report of Markup.language_path;