src/Pure/ML_Bootstrap.thy
Thu, 28 Sep 2023 20:07:30 +0200 wenzelm explicitly reject 'handle' with catch-all patterns;
Sat, 17 Dec 2022 19:19:10 +0100 wenzelm discontinued somewhat pointless dependency: avoid illusion of extra accuracy (see also 09fb749d1a1e and 0f750a6dc754);
Thu, 06 Sep 2018 14:08:35 +0200 wenzelm simplified signature (again, see 751bcf0473a7): e.g. relevant for non-Isabelle ML environments;
Mon, 27 Aug 2018 17:26:14 +0200 wenzelm tuned;
Mon, 27 Aug 2018 14:42:24 +0200 wenzelm support named ML environments, notably "Isabelle", "SML";
Sun, 26 Aug 2018 15:39:34 +0200 wenzelm clarified -- prefer new 'ML_export' command;
Sat, 25 Aug 2018 10:29:31 +0200 wenzelm retain original PolyML.pointerEq;
Wed, 06 Dec 2017 18:59:33 +0100 wenzelm prefer control symbol antiquotations;
Wed, 29 Nov 2017 10:27:56 +0100 wenzelm clarified dependencies: "isabelle build -S" should be invariant wrt. change of ML system or platform;
Fri, 21 Oct 2016 11:19:15 +0200 wenzelm proper type for Poly/ML development version;
Thu, 02 Jun 2016 15:52:45 +0200 wenzelm avoid stateful operations in virtual bootstrap, which presumably causes occasional crash of drule.ML due to inner syntax pp;
Sun, 10 Apr 2016 21:46:12 +0200 wenzelm more standard session build process, including browser_info;
Sat, 09 Apr 2016 16:16:05 +0200 wenzelm shared output primitives of physical/virtual Pure;
Thu, 07 Apr 2016 16:53:43 +0200 wenzelm more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use';
Wed, 06 Apr 2016 19:03:29 +0200 wenzelm virtual thread data via context, for proper support of Context.>> etc;
Wed, 06 Apr 2016 14:02:12 +0200 wenzelm clarified ML bootstrap environment;
less more (0) tip