src/Pure/term_items.ML
Tue, 18 Apr 2023 21:47:40 +0200 wenzelm more operations: avoid intermediate list;
Wed, 12 Apr 2023 10:42:23 +0200 wenzelm performance tuning: proper pointer_eq;
Tue, 11 Apr 2023 21:42:45 +0200 wenzelm misc tuning: follow Table() more closely;
Thu, 09 Sep 2021 22:12:05 +0200 wenzelm clarified signature;
Thu, 09 Sep 2021 15:45:27 +0200 wenzelm clarified modules;
less more (0) tip