| 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
|