| Thu, 29 Sep 2005 00:59:00 +0200 |
wenzelm |
back to simple 'defs' (cf. revision 1.79 of theory.ML);
|
file |
diff |
annotate
|
| Tue, 27 Sep 2005 14:41:41 +0200 |
obua |
corrected spelling bug
|
file |
diff |
annotate
|
| Tue, 27 Sep 2005 14:39:35 +0200 |
obua |
added defs disclaimer
|
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 22:15:10 +0200 |
wenzelm |
curried_lookup/update;
|
file |
diff |
annotate
|
| Mon, 01 Aug 2005 19:20:36 +0200 |
wenzelm |
chain_history: turned into runtime flag;
|
file |
diff |
annotate
|
| Thu, 28 Jul 2005 15:19:53 +0200 |
wenzelm |
Type.raw_instance, Type.raw_unify, Term.zero_var_indexesT;
|
file |
diff |
annotate
|
| Tue, 19 Jul 2005 17:21:49 +0200 |
wenzelm |
tuned interfaces declare, define, finalize, merge:
|
file |
diff |
annotate
|
| Thu, 14 Jul 2005 19:28:20 +0200 |
wenzelm |
use existing Inttab;
|
file |
diff |
annotate
|
| Thu, 14 Jul 2005 14:05:48 +0200 |
obua |
- fixed bug concerning the renaming of axiom names
|
file |
diff |
annotate
|
| Mon, 11 Jul 2005 14:52:55 +0200 |
obua |
Improved implementation of Defs.is_overloaded.
|
file |
diff |
annotate
|
| Thu, 07 Jul 2005 19:01:04 +0200 |
obua |
1) all theorems in Orderings can now be given as a parameter
|
file |
diff |
annotate
|
| Mon, 13 Jun 2005 21:28:57 +0200 |
obua |
internalize axiom names in Defs.define; compress types via Term.compress_type
|
file |
diff |
annotate
|
| Sat, 11 Jun 2005 12:55:25 +0200 |
obua |
further optimizations of cycle test
|
file |
diff |
annotate
|
| Tue, 07 Jun 2005 06:39:39 +0200 |
obua |
1) Fixed bug in Defs.merge_edges_1.
|
file |
diff |
annotate
|
| Fri, 03 Jun 2005 01:08:07 +0200 |
obua |
Integrates cycle detection in definitions with finalconsts
|
file |
diff |
annotate
|
| Wed, 01 Jun 2005 21:25:35 +0200 |
obua |
Preliminary version of defs.ML that does not check final consts.
|
file |
diff |
annotate
|
| Tue, 31 May 2005 19:32:41 +0200 |
obua |
Removed final_consts from theory data. Now const_deps deals with final
|
file |
diff |
annotate
|
| Mon, 30 May 2005 16:32:47 +0200 |
obua |
Infinite chains in definitions are now detected, too.
|
file |
diff |
annotate
|
| Sun, 29 May 2005 12:39:12 +0200 |
obua |
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
|
file |
diff |
annotate
|