| 2006-05-24 |
wenzelm |
2006-05-24 |
tuned;
|
file | diff | annotate |
| 2006-05-23 |
wenzelm |
2006-05-23 |
export plain_args;
tuned wellformed, normalize;
|
file | diff | annotate |
| 2006-05-22 |
wenzelm |
2006-05-22 |
specifications_of: lhs/rhs represented as typargs;
export pretty_const;
export dest;
more precise checking of lhs patterns;
more precise normalization;
misc cleanup;
|
file | diff | annotate |
| 2006-05-20 |
wenzelm |
2006-05-20 |
made smlnj happy;
|
file | diff | annotate |
| 2006-05-20 |
wenzelm |
2006-05-20 |
yet another re-implementation:
. maintain explicit mapping from unspecified to specified consts (no
dependency graph, no termination check, but direct reduction of
specifications);
. more precise checking of LHS patterns -- specialized patterns
(e.g. 'a => 'a instead of general 'a => 'b) impose global
restrictions;
|
file | diff | annotate |
| 2006-05-13 |
wenzelm |
2006-05-13 |
actually reject malformed defs;
added unchecked flag;
tuned;
|
file | diff | annotate |
| 2006-05-12 |
wenzelm |
2006-05-12 |
tuned;
|
file | diff | annotate |
| 2006-05-12 |
wenzelm |
2006-05-12 |
improved propagate_deps;
removed structs_less, which is actually unsound in conjunction with interdependent overloaded consts;
|
file | diff | annotate |
| 2006-05-11 |
wenzelm |
2006-05-11 |
allow dependencies of disjoint collections of instances;
major cleanup;
|
file | diff | annotate |
| 2006-05-08 |
wenzelm |
2006-05-08 |
simple substructure test for typargs (independent type constructors);
|
file | diff | annotate |
| 2006-05-05 |
wenzelm |
2006-05-05 |
specifications_of: more detailed information;
tuned;
|
file | diff | annotate |
| 2006-04-27 |
wenzelm |
2006-04-27 |
tuned basic list operators (flat, maps, map_filter);
|
file | diff | annotate |
| 2006-04-06 |
haftmann |
2006-04-06 |
exported specification names
|
file | diff | annotate |
| 2006-02-25 |
haftmann |
2006-02-25 |
added more detailed data to consts
|
file | diff | annotate |
| 2006-02-15 |
wenzelm |
2006-02-15 |
specifications_of: avoid partiality;
|
file | diff | annotate |
| 2006-02-15 |
haftmann |
2006-02-15 |
exported specifications_of
|
file | diff | annotate |
| 2006-02-12 |
wenzelm |
2006-02-12 |
simplified TableFun.join;
|
file | diff | annotate |
| 2005-10-27 |
wenzelm |
2005-10-27 |
removed inappropriate monomorphic test;
|
file | diff | annotate |
| 2005-10-08 |
wenzelm |
2005-10-08 |
more efficient check_specified, much less invocations;
Type.could_unify filter;
|
file | diff | annotate |
| 2005-09-29 |
wenzelm |
2005-09-29 |
make signature constraint actually work;
|
file | diff | annotate |
| 2005-09-29 |
wenzelm |
2005-09-29 |
activate signature constraints;
|
file | diff | annotate |
| 2005-09-29 |
wenzelm |
2005-09-29 |
back to simple 'defs' (cf. revision 1.79 of theory.ML);
renamed 'finals' to 'specified', share bookkeeping with defs;
added monomorphic;
|
file | diff | annotate |
| 2005-09-27 |
obua |
2005-09-27 |
corrected spelling bug
|
file | diff | annotate |
| 2005-09-27 |
obua |
2005-09-27 |
added defs disclaimer
|
file | diff | annotate |
| 2005-09-15 |
wenzelm |
2005-09-15 |
TableFun/Symtab: curried lookup and update;
|
file | diff | annotate |
| 2005-09-01 |
wenzelm |
2005-09-01 |
curried_lookup/update;
tuned;
|
file | diff | annotate |
| 2005-08-01 |
wenzelm |
2005-08-01 |
chain_history: turned into runtime flag;
added monomorphic;
removed (inefficient) fast_overloading_info;
Compress.typ;
tuned;
|
file | diff | annotate |
| 2005-07-28 |
wenzelm |
2005-07-28 |
Type.raw_instance, Type.raw_unify, Term.zero_var_indexesT;
|
file | diff | annotate |
| 2005-07-19 |
wenzelm |
2005-07-19 |
tuned interfaces declare, define, finalize, merge:
canonical argument order, produce errors;
tuned checkT';
|
file | diff | annotate |
| 2005-07-14 |
wenzelm |
2005-07-14 |
use existing Inttab;
|
file | diff | annotate |
| 2005-07-14 |
obua |
2005-07-14 |
- fixed bug concerning the renaming of axiom names
- introduced new function Defs.fast_overloading_info
|
file | diff | annotate |
| 2005-07-11 |
obua |
2005-07-11 |
Improved implementation of Defs.is_overloaded.
|
file | diff | annotate |
| 2005-07-07 |
obua |
2005-07-07 |
1) all theorems in Orderings can now be given as a parameter
2) new function Theory.defs_of
3) new functions Defs.overloading_info and Defs.is_overloaded
|
file | diff | annotate |
| 2005-06-13 |
obua |
2005-06-13 |
internalize axiom names in Defs.define; compress types via Term.compress_type
|
file | diff | annotate |
| 2005-06-11 |
obua |
2005-06-11 |
further optimizations of cycle test
|
file | diff | annotate |
| 2005-06-07 |
obua |
2005-06-07 |
1) Fixed bug in Defs.merge_edges_1.
2) Major optimization of Defs.define: do not store dependencies between constants that
cannot introduce cycles anyway. In that way, the cycle test adds almost no overhead to
theories that define their constants in HOL-light / HOL4 style.
3) Cleaned up Defs.graph, no superfluous name tags are stored anymore.
|
file | diff | annotate |
| 2005-06-03 |
obua |
2005-06-03 |
Integrates cycle detection in definitions with finalconsts
|
file | diff | annotate |
| 2005-06-01 |
obua |
2005-06-01 |
Preliminary version of defs.ML that does not check final consts.
|
file | diff | annotate |
| 2005-05-31 |
obua |
2005-05-31 |
Removed final_consts from theory data. Now const_deps deals with final
constants.
|
file | diff | annotate |
| 2005-05-30 |
obua |
2005-05-30 |
Infinite chains in definitions are now detected, too.
|
file | diff | annotate |
| 2005-05-29 |
obua |
2005-05-29 |
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
|
file | diff | annotate |