| 2010-06-01 |
wenzelm |
2010-06-01 |
arities: no need to maintain original codomain (cf. f795c1164708) -- completion happens in axclass.ML;
misc tuning;
|
file | diff | annotate |
| 2010-04-27 |
wenzelm |
2010-04-27 |
monotonic sort certification: sorts are no longer minimized at the kernel boundary, only when reading input from the end-user;
|
file | diff | annotate |
| 2010-04-25 |
wenzelm |
2010-04-25 |
replaced Sorts.rep_algebra by slightly more abstract selectors classes_of/arities_of;
|
file | diff | annotate |
| 2010-04-11 |
wenzelm |
2010-04-11 |
modernized datatype constructors;
|
file | diff | annotate |
| 2010-04-11 |
wenzelm |
2010-04-11 |
of_sort_derivation: weaken bypasses derivation for identical sort -- accomodate proof terms by krauss/schropp, for example;
|
file | diff | annotate |
| 2010-04-11 |
wenzelm |
2010-04-11 |
tuned;
|
file | diff | annotate |
| 2010-04-11 |
wenzelm |
2010-04-11 |
of_sort_derivation: pass-through full type information -- following the version by krauss/schropp;
|
file | diff | annotate |
| 2010-03-26 |
wenzelm |
2010-03-26 |
more efficient merge_algebra for important special cases -- tricky due to required completion if class algebra changes;
|
file | diff | annotate |
| 2010-03-25 |
wenzelm |
2010-03-25 |
Sorts.of_sort_derivation: do not use slow Graph.irreducible_paths here, which not always needed (SUBTLE CHANGE IN SEMANTICS);
officially export weaken as Sorts.classrel_derivation;
tuned comments;
|
file | diff | annotate |
| 2010-02-27 |
wenzelm |
2010-02-27 |
modernized structure Term_Ord;
|
file | diff | annotate |
| 2009-10-20 |
haftmann |
2009-10-20 |
replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
|
file | diff | annotate |
| 2009-09-30 |
wenzelm |
2009-09-30 |
removed dead code;
Sorts.of_sort_derivation: removed unused pp;
|
file | diff | annotate |
| 2009-07-06 |
wenzelm |
2009-07-06 |
witness_sorts: proper type witnesses for hyps, not invented "'hyp" variables;
|
file | diff | annotate |
| 2009-03-04 |
blanchet |
2009-03-04 |
Merge.
|
file | diff | annotate |
| 2009-03-04 |
blanchet |
2009-03-04 |
Merge.
|
file | diff | annotate |
| 2009-02-23 |
haftmann |
2009-02-23 |
stripped classrels_of, instances_of
|
file | diff | annotate |
| 2009-02-22 |
haftmann |
2009-02-22 |
handle NONE case in arity function properly
|
file | diff | annotate |
| 2009-02-22 |
haftmann |
2009-02-22 |
subalgebra: drop arities if desired
|
file | diff | annotate |
| 2009-02-18 |
haftmann |
2009-02-18 |
sort instances wrt. to class hierarchy
|
file | diff | annotate |
| 2008-12-31 |
wenzelm |
2008-12-31 |
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
tuned signature of structure Term;
|
file | diff | annotate |
| 2008-12-01 |
haftmann |
2008-12-01 |
more means for algebra projection
|
file | diff | annotate |
| 2008-10-22 |
haftmann |
2008-10-22 |
added meet_sort_typ
|
file | diff | annotate |
| 2008-10-16 |
wenzelm |
2008-10-16 |
added make, minimal_sorts;
|
file | diff | annotate |
| 2008-09-26 |
wenzelm |
2008-09-26 |
added subset operation;
|
file | diff | annotate |
| 2008-09-25 |
wenzelm |
2008-09-25 |
explicit type OrdList.T;
|
file | diff | annotate |
| 2008-07-11 |
wenzelm |
2008-07-11 |
Sorts.weaken: abstract argument;
tuned;
|
file | diff | annotate |
| 2008-07-11 |
haftmann |
2008-07-11 |
fixed layout
|
file | diff | annotate |
| 2008-07-08 |
haftmann |
2008-07-08 |
exported weaken combinator
|
file | diff | annotate |
| 2008-05-26 |
haftmann |
2008-05-26 |
proper NoSubsort CLASS_ERROR
|
file | diff | annotate |
| 2008-04-13 |
wenzelm |
2008-04-13 |
removed unused minimal_classes;
class_error: produce message only (formerly msg_class_error);
tuned;
|
file | diff | annotate |
| 2008-04-02 |
haftmann |
2008-04-02 |
canonical meet_sort operation
|
file | diff | annotate |
| 2008-03-19 |
haftmann |
2008-03-19 |
new class error case NoSubsort
|
file | diff | annotate |
| 2007-09-26 |
wenzelm |
2007-09-26 |
added minimize_sort, complete_sort;
|
file | diff | annotate |
| 2007-07-08 |
wenzelm |
2007-07-08 |
replaced exception TableFun/GraphFun.DUPS by TableFun/GraphFun.DUP;
|
file | diff | annotate |
| 2007-07-05 |
wenzelm |
2007-07-05 |
sort_le: tuned eq case;
|
file | diff | annotate |
| 2007-04-03 |
wenzelm |
2007-04-03 |
renamed of_sort_derivation record fields (avoid clash with Alice keywords);
|
file | diff | annotate |
| 2007-02-26 |
wenzelm |
2007-02-26 |
removed obsolete eq_set;
|
file | diff | annotate |
| 2007-01-26 |
haftmann |
2007-01-26 |
exported interface for explicit error messages
|
file | diff | annotate |
| 2007-01-25 |
haftmann |
2007-01-25 |
added explicit query function for arities to subalgebra projection
|
file | diff | annotate |
| 2006-12-29 |
wenzelm |
2006-12-29 |
classes: more direct way to achieve topological sorting;
renamed classes to all_classes;
added minimal_classes;
renamed project to subalgebra, tuned;
|
file | diff | annotate |
| 2006-12-29 |
haftmann |
2006-12-29 |
``classes`` now returns classes in topological order
|
file | diff | annotate |
| 2006-09-18 |
wenzelm |
2006-09-18 |
classes: maintain serial number;
|
file | diff | annotate |
| 2006-09-04 |
haftmann |
2006-09-04 |
proper project_sort
|
file | diff | annotate |
| 2006-09-01 |
haftmann |
2006-09-01 |
project_algebra yields sort projector
|
file | diff | annotate |
| 2006-08-17 |
haftmann |
2006-08-17 |
added all_super_classes
|
file | diff | annotate |
| 2006-07-03 |
wenzelm |
2006-07-03 |
project_algebra: norm_sort;
tuned;
|
file | diff | annotate |
| 2006-06-27 |
haftmann |
2006-06-27 |
added class projection
|
file | diff | annotate |
| 2006-05-16 |
wenzelm |
2006-05-16 |
abstract interfaces for type algebra;
tuned;
|
file | diff | annotate |
| 2006-05-07 |
wenzelm |
2006-05-07 |
tuned;
|
file | diff | annotate |
| 2006-05-05 |
wenzelm |
2006-05-05 |
added class_error and exception CLASS_ERROR (supercedes DOMAIN);
clarified of_class_derivation;
tuned witness_sorts;
|
file | diff | annotate |
| 2006-05-02 |
wenzelm |
2006-05-02 |
tuned;
|
file | diff | annotate |
| 2006-05-02 |
wenzelm |
2006-05-02 |
added domain_error;
added of_sort_derivation;
tuned;
|
file | diff | annotate |
| 2006-05-01 |
wenzelm |
2006-05-01 |
arities: maintain original codomain;
|
file | diff | annotate |
| 2006-04-30 |
wenzelm |
2006-04-30 |
moved certify_class/sort to type.ML;
added operations to build sort algebras (from type.ML);
tuned;
|
file | diff | annotate |
| 2006-04-27 |
wenzelm |
2006-04-27 |
tuned basic list operators (flat, maps, map_filter);
|
file | diff | annotate |
| 2006-04-25 |
wenzelm |
2006-04-25 |
added remove_sort;
|
file | diff | annotate |
| 2006-04-11 |
wenzelm |
2006-04-11 |
removed superclasses (see sign.ML);
|
file | diff | annotate |
| 2006-04-10 |
wenzelm |
2006-04-10 |
removed unused class_le_path, sort_less;
|
file | diff | annotate |
| 2006-02-06 |
wenzelm |
2006-02-06 |
TableFun: renamed xxx_multi to xxx_list;
|
file | diff | annotate |
| 2005-12-17 |
wenzelm |
2005-12-17 |
sort_distinct;
|
file | diff | annotate |