src/Tools/Code/code_target.ML
Tue, 03 Jan 2023 16:05:07 +0100 wenzelm clarified modules;
Thu, 23 Jun 2022 21:50:32 +0200 wenzelm more scalable generated files and code export, using Bytes.T;
Mon, 06 Dec 2021 15:34:54 +0100 wenzelm discontinued old-style {* verbatim *} tokens;
Wed, 20 Oct 2021 18:13:17 +0200 wenzelm discontinued obsolete "val extend = I" for data slots;
Fri, 21 May 2021 12:29:29 +0200 wenzelm clarified modules;
Mon, 07 Dec 2020 16:09:06 +0100 wenzelm more accurate markup (refining 1c59b555ac4a);
less more (0) -100 -30 -10 -6 tip