src/Pure/term_ord.ML
Thu, 30 Nov 2023 20:11:34 +0100 wenzelm reduce redundancy: avoid huge lists;
Wed, 19 Apr 2023 14:48:43 +0200 wenzelm minor performance tuning: recursive check of pointer_eq;
Tue, 18 Apr 2023 12:23:37 +0200 wenzelm backout 4a174bea55e2;
Tue, 28 Mar 2023 18:10:45 +0200 wenzelm tuned signature: more uniform structure Key;
Tue, 28 Mar 2023 17:59:54 +0200 wenzelm prefer Sortset.T for shyps;
Tue, 28 Mar 2023 17:51:21 +0200 wenzelm tuned;
Mon, 27 Mar 2023 21:48:47 +0200 wenzelm performance tuning: prefer functor Set() over Table();
Thu, 09 Sep 2021 15:45:27 +0200 wenzelm clarified modules;
Thu, 09 Sep 2021 14:50:26 +0200 wenzelm clarified set of items with order of addition;
Thu, 09 Sep 2021 12:33:14 +0200 wenzelm clarified signature;
Thu, 09 Sep 2021 10:40:57 +0200 wenzelm tuned;
Tue, 07 Sep 2021 20:27:06 +0200 wenzelm pointer_eq_ord: minor performance tuning;
Fri, 18 Jun 2021 12:13:09 +0200 wenzelm tuned;
Tue, 20 Aug 2019 11:01:05 +0200 wenzelm clarified signature;
Thu, 01 Feb 2018 15:31:25 +0100 wenzelm clarified signature: prefer proper order operation;
Wed, 13 Jul 2011 20:36:18 +0200 wenzelm sub-structural sharing after Syntax.check phase, with global interning of logical entities (the latter is relevant when bypassing default parsing via YXML);
Tue, 20 Jul 2010 14:44:33 +0200 wenzelm eliminated old-style sys_error/SYS_ERROR in favour of exception Fail -- after careful checking that there is no overlap with existing handling of that;
Sat, 27 Feb 2010 23:13:01 +0100 wenzelm modernized structure Term_Ord;
Sat, 27 Feb 2010 22:52:06 +0100 wenzelm further standard instances of functor Graph;
Sat, 27 Feb 2010 21:56:55 +0100 wenzelm just one copy of structure Term_Graph (in Pure);
Thu, 01 Oct 2009 22:39:58 +0200 wenzelm added term_cache;
Thu, 09 Jul 2009 22:36:11 +0200 wenzelm Sorttab in Pure;
Thu, 09 Jul 2009 22:01:41 +0200 wenzelm renamed functor TableFun to Table, and GraphFun to Graph;
Wed, 31 Dec 2008 15:30:10 +0100 wenzelm moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
less more (0) tip