| Mon, 21 Oct 2019 16:32:10 +0200 |
wenzelm |
export constdefs according to defs.ML;
|
file |
diff |
annotate
|
| Tue, 20 Aug 2019 11:01:05 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Thu, 14 Jan 2016 16:45:13 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 14 Jan 2016 13:51:13 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 14 Jan 2016 12:20:49 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 20 Dec 2015 13:06:26 +0100 |
wenzelm |
renamed Pretty.str_of to Pretty.unformatted_string_of to emphasize its meaning;
|
file |
diff |
annotate
|
| Fri, 25 Sep 2015 19:28:33 +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
|
| Thu, 24 Sep 2015 23:33:29 +0200 |
wenzelm |
more explicit Defs.context: use proper name spaces as far as possible;
|
file |
diff |
annotate
|
| Thu, 24 Sep 2015 13:33:42 +0200 |
wenzelm |
explicit indication of overloaded typedefs;
|
file |
diff |
annotate
|
| Tue, 22 Sep 2015 22:42:48 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 22 Sep 2015 20:29:20 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 22 Sep 2015 20:21:53 +0200 |
wenzelm |
tuned output;
|
file |
diff |
annotate
|
| Tue, 22 Sep 2015 16:49:56 +0200 |
wenzelm |
renamed Defs.node to Defs.item;
|
file |
diff |
annotate
|
| Tue, 22 Sep 2015 14:32:23 +0200 |
wenzelm |
HOL typedef with explicit dependency checks according to Ondrey Kuncar, 07-Jul-2015, 16-Jul-2015, 30-Jul-2015;
|
file |
diff |
annotate
|
| Mon, 24 Nov 2014 20:06:51 +0100 |
wenzelm |
removed odd remains of structural containment checks, which stem from an older approach (see also 3ad1b289f21b, 3ae3cc4b1eac, 423af2e013b8, bad13b32c0f3, ccd6de95f4a6);
|
file |
diff |
annotate
|
| Sat, 05 Jul 2014 13:21:53 +0200 |
wenzelm |
proper plain_args to ensure that multi-argument overloading cannot escape pattern restriction (despite more liberal structural containment before 3ae3cc4b1eac);
|
file |
diff |
annotate
|
| Tue, 11 Mar 2014 10:14:45 +0100 |
wenzelm |
minor performance tuning via fast matching filter;
|
file |
diff |
annotate
|
| Mon, 17 Feb 2014 20:19:02 +0100 |
wenzelm |
more informative error;
|
file |
diff |
annotate
|
| Mon, 18 Apr 2011 14:05:39 +0200 |
wenzelm |
pass plain Proof.context for pretty printing;
|
file |
diff |
annotate
|
| Mon, 18 Apr 2011 11:44:39 +0200 |
wenzelm |
pass plain Proof.context for pretty printing;
|
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
|
| Sat, 20 Mar 2010 17:33:11 +0100 |
wenzelm |
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
|
file |
diff |
annotate
|
| Mon, 16 Nov 2009 13:53:02 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 15 Nov 2009 20:39:22 +0100 |
wenzelm |
primitive defs: clarified def (axiom name) vs. description;
|
file |
diff |
annotate
|
| Wed, 30 Sep 2009 22:24:57 +0200 |
wenzelm |
eliminated redundant parameters;
|
file |
diff |
annotate
|
| Sat, 18 Jul 2009 00:34:22 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 17 Jul 2009 23:11:40 +0200 |
wenzelm |
tuned/modernized Envir.subst_XXX;
|
file |
diff |
annotate
|
| Wed, 21 Jan 2009 23:21:44 +0100 |
wenzelm |
removed Ids;
|
file |
diff |
annotate
|
| Mon, 01 Oct 2007 15:14:54 +0200 |
wenzelm |
tuned message;
|
file |
diff |
annotate
|
| Thu, 09 Aug 2007 15:52:54 +0200 |
haftmann |
new access interface in defs.ML
|
file |
diff |
annotate
|
| Thu, 21 Sep 2006 19:04:49 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 17 Aug 2006 09:24:48 +0200 |
haftmann |
renamed module to thyname
|
file |
diff |
annotate
|
| Wed, 07 Jun 2006 02:01:28 +0200 |
wenzelm |
renamed Type.(un)varifyT to Logic.(un)varifyT;
|
file |
diff |
annotate
|
| Fri, 02 Jun 2006 16:06:19 +0200 |
wenzelm |
merge: always normalize (and check!) reductions;
|
file |
diff |
annotate
|
| Fri, 26 May 2006 22:20:03 +0200 |
wenzelm |
separate checks for acyclic/wellformed;
|
file |
diff |
annotate
|
| Thu, 25 May 2006 16:51:39 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 24 May 2006 22:04:06 +0200 |
wenzelm |
made smlnj happy;
|
file |
diff |
annotate
|
| Wed, 24 May 2006 21:58:09 +0200 |
wenzelm |
wellformed: be less ambitious about structural containment;
|
file |
diff |
annotate
|
| Wed, 24 May 2006 01:05:01 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 23 May 2006 13:55:01 +0200 |
wenzelm |
export plain_args;
|
file |
diff |
annotate
|
| Mon, 22 May 2006 22:29:15 +0200 |
wenzelm |
specifications_of: lhs/rhs represented as typargs;
|
file |
diff |
annotate
|
| Sat, 20 May 2006 23:45:37 +0200 |
wenzelm |
made smlnj happy;
|
file |
diff |
annotate
|
| Sat, 20 May 2006 23:37:02 +0200 |
wenzelm |
yet another re-implementation:
|
file |
diff |
annotate
|
| Sat, 13 May 2006 02:51:37 +0200 |
wenzelm |
actually reject malformed defs;
|
file |
diff |
annotate
|
| Fri, 12 May 2006 18:11:09 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 12 May 2006 01:01:08 +0200 |
wenzelm |
improved propagate_deps;
|
file |
diff |
annotate
|
| Thu, 11 May 2006 19:15:13 +0200 |
wenzelm |
allow dependencies of disjoint collections of instances;
|
file |
diff |
annotate
|
| Mon, 08 May 2006 17:40:06 +0200 |
wenzelm |
simple substructure test for typargs (independent type constructors);
|
file |
diff |
annotate
|
| Fri, 05 May 2006 19:32:33 +0200 |
wenzelm |
specifications_of: more detailed information;
|
file |
diff |
annotate
|
| Thu, 27 Apr 2006 15:06:35 +0200 |
wenzelm |
tuned basic list operators (flat, maps, map_filter);
|
file |
diff |
annotate
|
| Thu, 06 Apr 2006 16:07:44 +0200 |
haftmann |
exported specification names
|
file |
diff |
annotate
|
| Sat, 25 Feb 2006 15:11:35 +0100 |
haftmann |
added more detailed data to consts
|
file |
diff |
annotate
|
| Wed, 15 Feb 2006 21:35:00 +0100 |
wenzelm |
specifications_of: avoid partiality;
|
file |
diff |
annotate
|
| Wed, 15 Feb 2006 17:09:06 +0100 |
haftmann |
exported specifications_of
|
file |
diff |
annotate
|
| Sun, 12 Feb 2006 21:34:18 +0100 |
wenzelm |
simplified TableFun.join;
|
file |
diff |
annotate
|
| Thu, 27 Oct 2005 13:54:42 +0200 |
wenzelm |
removed inappropriate monomorphic test;
|
file |
diff |
annotate
|
| Sat, 08 Oct 2005 22:39:41 +0200 |
wenzelm |
more efficient check_specified, much less invocations;
|
file |
diff |
annotate
|
| Thu, 29 Sep 2005 01:12:16 +0200 |
wenzelm |
make signature constraint actually work;
|
file |
diff |
annotate
|
| Thu, 29 Sep 2005 01:09:39 +0200 |
wenzelm |
activate signature constraints;
|
file |
diff |
annotate
|
| 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
|