src/Pure/sorts.ML
Tue, 09 Jan 2024 11:57:16 +0100 wenzelm clarified modules;
Sat, 30 Dec 2023 21:40:48 +0100 wenzelm tuned whitespace;
Sat, 30 Dec 2023 21:35:00 +0100 wenzelm clarified signature;
Tue, 18 Apr 2023 15:56:16 +0200 wenzelm Thm.shared context: speed-up low-level inferences;
Tue, 18 Apr 2023 12:23:37 +0200 wenzelm backout 4a174bea55e2;
Tue, 28 Mar 2023 17:59:54 +0200 wenzelm prefer Sortset.T for shyps;
Sat, 04 Sep 2021 22:05:35 +0200 wenzelm clarified signature;
Sat, 04 Sep 2021 21:25:08 +0200 wenzelm clarified signature;
Mon, 09 Mar 2020 11:52:28 +0100 wenzelm tuned signature;
Mon, 17 Feb 2020 20:35:04 +0100 wenzelm proper sort constraints for strip_shyps, for sort relations used in minimization;
Sat, 26 May 2018 22:02:25 +0200 wenzelm export sort algebra;
Tue, 08 Mar 2016 21:07:47 +0100 haftmann provide explicit hint concering uniqueness of derivation
Fri, 25 Sep 2015 19:23:17 +0200 wenzelm tuned;
Fri, 25 Sep 2015 19:13:47 +0200 wenzelm tuned signature: eliminated pointless type Context.pretty;
Mon, 16 Jul 2012 21:20:56 +0200 wenzelm more direct Sorts.has_instance;
Sun, 18 Mar 2012 13:04:22 +0100 wenzelm maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
Thu, 23 Feb 2012 15:49:40 +0100 wenzelm clarified Graph.restrict (formerly Graph.subgraph) based on public graph operations;
Sun, 20 Nov 2011 15:21:22 +0100 wenzelm clarified certify vs. sharing;
Sat, 20 Aug 2011 23:35:30 +0200 wenzelm refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
Wed, 13 Jul 2011 16:42:14 +0200 wenzelm Table.lookup_key and Graph.get_entry allow to retrieve the original key, which is not necessarily identical to the given one;
Mon, 18 Apr 2011 13:26:39 +0200 wenzelm pass plain Proof.context for pretty printing;
Mon, 18 Apr 2011 12:04:21 +0200 wenzelm simplified Sorts.class_error: plain Proof.context;
Mon, 18 Apr 2011 11:13:29 +0200 wenzelm simplified pretty printing context, which is only required for certain kernel operations;
Fri, 24 Sep 2010 15:53:13 +0200 wenzelm modernized structure Ord_List;
Wed, 01 Sep 2010 15:33:59 +0200 haftmann replaced Table.map' by Table.map
Tue, 01 Jun 2010 22:19:17 +0200 wenzelm arities: no need to maintain original codomain (cf. f795c1164708) -- completion happens in axclass.ML;
Tue, 27 Apr 2010 21:46:10 +0200 wenzelm monotonic sort certification: sorts are no longer minimized at the kernel boundary, only when reading input from the end-user;
Sun, 25 Apr 2010 21:18:04 +0200 wenzelm replaced Sorts.rep_algebra by slightly more abstract selectors classes_of/arities_of;
Sun, 11 Apr 2010 14:06:35 +0200 wenzelm modernized datatype constructors;
Sun, 11 Apr 2010 14:04:10 +0200 wenzelm of_sort_derivation: weaken bypasses derivation for identical sort -- accomodate proof terms by krauss/schropp, for example;
Sun, 11 Apr 2010 13:13:23 +0200 wenzelm tuned;
Sun, 11 Apr 2010 13:08:14 +0200 wenzelm of_sort_derivation: pass-through full type information -- following the version by krauss/schropp;
Fri, 26 Mar 2010 20:28:15 +0100 wenzelm more efficient merge_algebra for important special cases -- tricky due to required completion if class algebra changes;
Thu, 25 Mar 2010 21:27:04 +0100 wenzelm Sorts.of_sort_derivation: do not use slow Graph.irreducible_paths here, which not always needed (SUBTLE CHANGE IN SEMANTICS);
Sat, 27 Feb 2010 23:13:01 +0100 wenzelm modernized structure Term_Ord;
Tue, 20 Oct 2009 16:13:01 +0200 haftmann replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
Wed, 30 Sep 2009 22:53:33 +0200 wenzelm removed dead code;
Mon, 06 Jul 2009 22:41:00 +0200 wenzelm witness_sorts: proper type witnesses for hyps, not invented "'hyp" variables;
Wed, 04 Mar 2009 11:05:29 +0100 blanchet Merge.
Wed, 04 Mar 2009 10:45:52 +0100 blanchet Merge.
Mon, 23 Feb 2009 10:07:57 +0100 haftmann stripped classrels_of, instances_of
Sun, 22 Feb 2009 18:16:32 +0100 haftmann handle NONE case in arity function properly
Sun, 22 Feb 2009 18:00:05 +0100 haftmann subalgebra: drop arities if desired
Wed, 18 Feb 2009 19:18:33 +0100 haftmann sort instances wrt. to class hierarchy
Wed, 31 Dec 2008 15:30:10 +0100 wenzelm moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
Mon, 01 Dec 2008 12:17:00 +0100 haftmann more means for algebra projection
Wed, 22 Oct 2008 14:15:47 +0200 haftmann added meet_sort_typ
Thu, 16 Oct 2008 22:44:32 +0200 wenzelm added make, minimal_sorts;
Fri, 26 Sep 2008 17:24:15 +0200 wenzelm added subset operation;
Thu, 25 Sep 2008 13:21:13 +0200 wenzelm explicit type OrdList.T;
Fri, 11 Jul 2008 23:17:25 +0200 wenzelm Sorts.weaken: abstract argument;
Fri, 11 Jul 2008 09:02:31 +0200 haftmann fixed layout
Tue, 08 Jul 2008 18:13:11 +0200 haftmann exported weaken combinator
Mon, 26 May 2008 17:55:35 +0200 haftmann proper NoSubsort CLASS_ERROR
Sun, 13 Apr 2008 16:40:05 +0200 wenzelm removed unused minimal_classes;
Wed, 02 Apr 2008 15:58:40 +0200 haftmann canonical meet_sort operation
Wed, 19 Mar 2008 07:20:30 +0100 haftmann new class error case NoSubsort
Wed, 26 Sep 2007 20:50:34 +0200 wenzelm added minimize_sort, complete_sort;
Sun, 08 Jul 2007 19:51:58 +0200 wenzelm replaced exception TableFun/GraphFun.DUPS by TableFun/GraphFun.DUP;
Thu, 05 Jul 2007 00:06:24 +0200 wenzelm sort_le: tuned eq case;
less more (0) -100 -60 tip