| Tue, 09 Jan 2024 11:57:16 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Sat, 30 Dec 2023 21:40:48 +0100 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Sat, 30 Dec 2023 21:35:00 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Tue, 18 Apr 2023 15:56:16 +0200 |
wenzelm |
Thm.shared context: speed-up low-level inferences;
|
file |
diff |
annotate
|
| Tue, 18 Apr 2023 12:23:37 +0200 |
wenzelm |
backout 4a174bea55e2;
|
file |
diff |
annotate
|
| Tue, 28 Mar 2023 17:59:54 +0200 |
wenzelm |
prefer Sortset.T for shyps;
|
file |
diff |
annotate
|
| Sat, 04 Sep 2021 22:05:35 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sat, 04 Sep 2021 21:25:08 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Mon, 09 Mar 2020 11:52:28 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 17 Feb 2020 20:35:04 +0100 |
wenzelm |
proper sort constraints for strip_shyps, for sort relations used in minimization;
|
file |
diff |
annotate
|
| Sat, 26 May 2018 22:02:25 +0200 |
wenzelm |
export sort algebra;
|
file |
diff |
annotate
|
| Tue, 08 Mar 2016 21:07:47 +0100 |
haftmann |
provide explicit hint concering uniqueness of derivation
|
file |
diff |
annotate
|
| Fri, 25 Sep 2015 19:23:17 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 25 Sep 2015 19:13:47 +0200 |
wenzelm |
tuned signature: eliminated pointless type Context.pretty;
|
file |
diff |
annotate
|
| Mon, 16 Jul 2012 21:20:56 +0200 |
wenzelm |
more direct Sorts.has_instance;
|
file |
diff |
annotate
|
| Sun, 18 Mar 2012 13:04:22 +0100 |
wenzelm |
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
|
file |
diff |
annotate
|
| Thu, 23 Feb 2012 15:49:40 +0100 |
wenzelm |
clarified Graph.restrict (formerly Graph.subgraph) based on public graph operations;
|
file |
diff |
annotate
|
| Sun, 20 Nov 2011 15:21:22 +0100 |
wenzelm |
clarified certify vs. sharing;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Mon, 18 Apr 2011 13:26:39 +0200 |
wenzelm |
pass plain Proof.context for pretty printing;
|
file |
diff |
annotate
|
| Mon, 18 Apr 2011 12:04:21 +0200 |
wenzelm |
simplified Sorts.class_error: plain Proof.context;
|
file |
diff |
annotate
|
| Mon, 18 Apr 2011 11:13:29 +0200 |
wenzelm |
simplified pretty printing context, which is only required for certain kernel operations;
|
file |
diff |
annotate
|
| Fri, 24 Sep 2010 15:53:13 +0200 |
wenzelm |
modernized structure Ord_List;
|
file |
diff |
annotate
|
| Wed, 01 Sep 2010 15:33:59 +0200 |
haftmann |
replaced Table.map' by Table.map
|
file |
diff |
annotate
|
| Tue, 01 Jun 2010 22:19:17 +0200 |
wenzelm |
arities: no need to maintain original codomain (cf. f795c1164708) -- completion happens in axclass.ML;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Sun, 25 Apr 2010 21:18:04 +0200 |
wenzelm |
replaced Sorts.rep_algebra by slightly more abstract selectors classes_of/arities_of;
|
file |
diff |
annotate
|
| Sun, 11 Apr 2010 14:06:35 +0200 |
wenzelm |
modernized datatype constructors;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Sun, 11 Apr 2010 13:13:23 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 11 Apr 2010 13:08:14 +0200 |
wenzelm |
of_sort_derivation: pass-through full type information -- following the version by krauss/schropp;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| 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);
|
file |
diff |
annotate
|
| Sat, 27 Feb 2010 23:13:01 +0100 |
wenzelm |
modernized structure Term_Ord;
|
file |
diff |
annotate
|
| Tue, 20 Oct 2009 16:13:01 +0200 |
haftmann |
replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
|
file |
diff |
annotate
|
| Wed, 30 Sep 2009 22:53:33 +0200 |
wenzelm |
removed dead code;
|
file |
diff |
annotate
|
| Mon, 06 Jul 2009 22:41:00 +0200 |
wenzelm |
witness_sorts: proper type witnesses for hyps, not invented "'hyp" variables;
|
file |
diff |
annotate
|
| Wed, 04 Mar 2009 11:05:29 +0100 |
blanchet |
Merge.
|
file |
diff |
annotate
|
| Wed, 04 Mar 2009 10:45:52 +0100 |
blanchet |
Merge.
|
file |
diff |
annotate
|
| Mon, 23 Feb 2009 10:07:57 +0100 |
haftmann |
stripped classrels_of, instances_of
|
file |
diff |
annotate
|
| Sun, 22 Feb 2009 18:16:32 +0100 |
haftmann |
handle NONE case in arity function properly
|
file |
diff |
annotate
|
| Sun, 22 Feb 2009 18:00:05 +0100 |
haftmann |
subalgebra: drop arities if desired
|
file |
diff |
annotate
|
| Wed, 18 Feb 2009 19:18:33 +0100 |
haftmann |
sort instances wrt. to class hierarchy
|
file |
diff |
annotate
|
| Wed, 31 Dec 2008 15:30:10 +0100 |
wenzelm |
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
|
file |
diff |
annotate
|
| Mon, 01 Dec 2008 12:17:00 +0100 |
haftmann |
more means for algebra projection
|
file |
diff |
annotate
|
| Wed, 22 Oct 2008 14:15:47 +0200 |
haftmann |
added meet_sort_typ
|
file |
diff |
annotate
|
| Thu, 16 Oct 2008 22:44:32 +0200 |
wenzelm |
added make, minimal_sorts;
|
file |
diff |
annotate
|
| Fri, 26 Sep 2008 17:24:15 +0200 |
wenzelm |
added subset operation;
|
file |
diff |
annotate
|
| Thu, 25 Sep 2008 13:21:13 +0200 |
wenzelm |
explicit type OrdList.T;
|
file |
diff |
annotate
|
| Fri, 11 Jul 2008 23:17:25 +0200 |
wenzelm |
Sorts.weaken: abstract argument;
|
file |
diff |
annotate
|
| Fri, 11 Jul 2008 09:02:31 +0200 |
haftmann |
fixed layout
|
file |
diff |
annotate
|
| Tue, 08 Jul 2008 18:13:11 +0200 |
haftmann |
exported weaken combinator
|
file |
diff |
annotate
|
| Mon, 26 May 2008 17:55:35 +0200 |
haftmann |
proper NoSubsort CLASS_ERROR
|
file |
diff |
annotate
|
| Sun, 13 Apr 2008 16:40:05 +0200 |
wenzelm |
removed unused minimal_classes;
|
file |
diff |
annotate
|
| Wed, 02 Apr 2008 15:58:40 +0200 |
haftmann |
canonical meet_sort operation
|
file |
diff |
annotate
|
| Wed, 19 Mar 2008 07:20:30 +0100 |
haftmann |
new class error case NoSubsort
|
file |
diff |
annotate
|
| Wed, 26 Sep 2007 20:50:34 +0200 |
wenzelm |
added minimize_sort, complete_sort;
|
file |
diff |
annotate
|
| Sun, 08 Jul 2007 19:51:58 +0200 |
wenzelm |
replaced exception TableFun/GraphFun.DUPS by TableFun/GraphFun.DUP;
|
file |
diff |
annotate
|
| Thu, 05 Jul 2007 00:06:24 +0200 |
wenzelm |
sort_le: tuned eq case;
|
file |
diff |
annotate
|
| Tue, 03 Apr 2007 19:24:16 +0200 |
wenzelm |
renamed of_sort_derivation record fields (avoid clash with Alice keywords);
|
file |
diff |
annotate
|
| Mon, 26 Feb 2007 23:18:29 +0100 |
wenzelm |
removed obsolete eq_set;
|
file |
diff |
annotate
|
| Fri, 26 Jan 2007 13:59:03 +0100 |
haftmann |
exported interface for explicit error messages
|
file |
diff |
annotate
|
| Thu, 25 Jan 2007 09:32:46 +0100 |
haftmann |
added explicit query function for arities to subalgebra projection
|
file |
diff |
annotate
|
| Fri, 29 Dec 2006 17:24:44 +0100 |
wenzelm |
classes: more direct way to achieve topological sorting;
|
file |
diff |
annotate
|
| Fri, 29 Dec 2006 12:11:03 +0100 |
haftmann |
``classes`` now returns classes in topological order
|
file |
diff |
annotate
|
| Mon, 18 Sep 2006 19:12:45 +0200 |
wenzelm |
classes: maintain serial number;
|
file |
diff |
annotate
|
| Mon, 04 Sep 2006 08:17:28 +0200 |
haftmann |
proper project_sort
|
file |
diff |
annotate
|
| Fri, 01 Sep 2006 08:36:53 +0200 |
haftmann |
project_algebra yields sort projector
|
file |
diff |
annotate
|
| Thu, 17 Aug 2006 09:24:49 +0200 |
haftmann |
added all_super_classes
|
file |
diff |
annotate
|
| Mon, 03 Jul 2006 19:33:07 +0200 |
wenzelm |
project_algebra: norm_sort;
|
file |
diff |
annotate
|
| Tue, 27 Jun 2006 10:09:48 +0200 |
haftmann |
added class projection
|
file |
diff |
annotate
|
| Tue, 16 May 2006 13:01:28 +0200 |
wenzelm |
abstract interfaces for type algebra;
|
file |
diff |
annotate
|
| Sun, 07 May 2006 00:21:13 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 05 May 2006 21:59:46 +0200 |
wenzelm |
added class_error and exception CLASS_ERROR (supercedes DOMAIN);
|
file |
diff |
annotate
|
| Tue, 02 May 2006 00:33:40 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 02 May 2006 00:20:38 +0200 |
wenzelm |
added domain_error;
|
file |
diff |
annotate
|
| Mon, 01 May 2006 17:05:12 +0200 |
wenzelm |
arities: maintain original codomain;
|
file |
diff |
annotate
|
| Sun, 30 Apr 2006 22:50:08 +0200 |
wenzelm |
moved certify_class/sort to type.ML;
|
file |
diff |
annotate
|
| Thu, 27 Apr 2006 15:06:35 +0200 |
wenzelm |
tuned basic list operators (flat, maps, map_filter);
|
file |
diff |
annotate
|
| Tue, 25 Apr 2006 22:23:17 +0200 |
wenzelm |
added remove_sort;
|
file |
diff |
annotate
|
| Tue, 11 Apr 2006 16:00:05 +0200 |
wenzelm |
removed superclasses (see sign.ML);
|
file |
diff |
annotate
|
| Mon, 10 Apr 2006 00:33:52 +0200 |
wenzelm |
removed unused class_le_path, sort_less;
|
file |
diff |
annotate
|
| Mon, 06 Feb 2006 20:58:57 +0100 |
wenzelm |
TableFun: renamed xxx_multi to xxx_list;
|
file |
diff |
annotate
|
| Sat, 17 Dec 2005 01:00:40 +0100 |
wenzelm |
sort_distinct;
|
file |
diff |
annotate
|
| Tue, 04 Oct 2005 19:01:37 +0200 |
wenzelm |
minor tweaks for Poplog/ML;
|
file |
diff |
annotate
|
| Thu, 15 Sep 2005 17:16:56 +0200 |
wenzelm |
TableFun/Symtab: curried lookup and update;
|
file |
diff |
annotate
|
| Thu, 01 Sep 2005 18:48:50 +0200 |
wenzelm |
curried_lookup/update;
|
file |
diff |
annotate
|
| Mon, 29 Aug 2005 16:18:04 +0200 |
wenzelm |
use AList operations;
|
file |
diff |
annotate
|
| Sun, 28 Aug 2005 09:36:18 +0200 |
haftmann |
added superclasses, class_le_path
|
file |
diff |
annotate
|
| Tue, 19 Jul 2005 17:21:53 +0200 |
wenzelm |
tuned norm_sort, mg_domain;
|
file |
diff |
annotate
|
| Wed, 29 Jun 2005 15:13:28 +0200 |
wenzelm |
removed obsolete eq_sort, mem_sort, subset_sort, eq_set_sort, ins_sort, union_sort, rems_sort;
|
file |
diff |
annotate
|
| Wed, 15 Jun 2005 14:59:25 +0200 |
haftmann |
(undone experimental changes)
|
file |
diff |
annotate
|
| Wed, 15 Jun 2005 14:56:26 +0200 |
haftmann |
subclassing done
|
file |
diff |
annotate
|
| Thu, 03 Mar 2005 12:43:01 +0100 |
skalberg |
Move towards standard functions.
|
file |
diff |
annotate
|
| Sun, 13 Feb 2005 17:15:14 +0100 |
skalberg |
Deleted Library.option type.
|
file |
diff |
annotate
|
| Mon, 21 Jun 2004 16:40:08 +0200 |
wenzelm |
added certify_class/sort;
|
file |
diff |
annotate
|
| Sat, 05 Jun 2004 13:06:39 +0200 |
wenzelm |
tuned comments;
|
file |
diff |
annotate
|
| Sat, 29 May 2004 15:03:59 +0200 |
wenzelm |
improved output; refer to Pretty.pp;
|
file |
diff |
annotate
|
| Fri, 21 May 2004 21:21:51 +0200 |
wenzelm |
incorporate sort ops from term.ML; use Graph.T; misc cleanup;
|
file |
diff |
annotate
|
| Fri, 07 Jul 2000 21:51:52 +0200 |
wenzelm |
inter_sort: keep normal!
|
file |
diff |
annotate
|
| Wed, 29 Sep 1999 14:03:57 +0200 |
wenzelm |
mg_domain: exception DOMAIN;
|
file |
diff |
annotate
|
| Fri, 23 Jul 1999 16:50:55 +0200 |
wenzelm |
replace assoc lists by Symtab.table;
|
file |
diff |
annotate
|
| Mon, 06 Oct 1997 18:39:54 +0200 |
wenzelm |
now uses Syntax.simple_str_of_sort;
|
file |
diff |
annotate
|
| Wed, 06 Aug 1997 15:07:53 +0200 |
wenzelm |
added str_of_classrel;
|
file |
diff |
annotate
|
| Fri, 18 Apr 1997 11:57:51 +0200 |
wenzelm |
removed least_sort;
|
file |
diff |
annotate
|
| Wed, 16 Apr 1997 18:14:43 +0200 |
wenzelm |
Type classes and sorts (isolated from type.ML).
|
file |
diff |
annotate
|