| Thu, 07 Apr 2011 21:23:57 +0200 |
wenzelm |
constant =?= no longer exists (cf. 8c09e1fa24a7);
|
file |
diff |
annotate
|
| Thu, 30 Dec 2010 22:34:53 +0100 |
wenzelm |
uniform treatment of type vs. term environment (cf. b654fa27fbc4);
|
file |
diff |
annotate
|
| Fri, 15 Oct 2010 17:21:07 +0100 |
paulson |
prevention of self-referential type environments
|
file |
diff |
annotate
|
| Mon, 06 Sep 2010 21:33:19 +0200 |
wenzelm |
more explicit indication of Config.raw options, which are only needed for bootstrapping Pure;
|
file |
diff |
annotate
|
| Fri, 03 Sep 2010 16:09:12 +0200 |
wenzelm |
more explicit Config.declare vs. Config.declare_global;
|
file |
diff |
annotate
|
| Mon, 05 Jul 2010 14:21:30 +0100 |
paulson |
Unification (flexflex) bug fix; making "auto" deterministic
|
file |
diff |
annotate
|
| Tue, 29 Jun 2010 22:59:29 +0200 |
wenzelm |
fail with low-level exception, not user error;
|
file |
diff |
annotate
|
| Tue, 29 Jun 2010 21:56:31 +0200 |
wenzelm |
eliminated some unused bindings;
|
file |
diff |
annotate
|
| Tue, 29 Jun 2010 21:46:47 +0200 |
wenzelm |
recovered some indentation from the depths of time;
|
file |
diff |
annotate
|
| Mon, 10 May 2010 20:53:06 +0200 |
wenzelm |
renamed Config.get_thy to Config.get_global etc. to indicate that this is not the real thing;
|
file |
diff |
annotate
|
| Sun, 28 Mar 2010 16:59:06 +0200 |
wenzelm |
static defaults for configuration options;
|
file |
diff |
annotate
|
| Sat, 27 Feb 2010 23:13:01 +0100 |
wenzelm |
modernized structure Term_Ord;
|
file |
diff |
annotate
|
| Thu, 29 Oct 2009 17:58:26 +0100 |
wenzelm |
standardized filter/filter_out;
|
file |
diff |
annotate
|
| Thu, 22 Oct 2009 13:48:06 +0200 |
haftmann |
map_range (and map_index) combinator
|
file |
diff |
annotate
|
| Tue, 29 Sep 2009 11:49:22 +0200 |
wenzelm |
explicit indication of Unsynchronized.ref;
|
file |
diff |
annotate
|
| Fri, 17 Jul 2009 21:33:00 +0200 |
wenzelm |
tuned/modernized Envir operations;
|
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
|
| Tue, 09 Sep 2008 16:15:25 +0200 |
paulson |
Increasing the default limits in order to prevent unnecessary failures.
|
file |
diff |
annotate
|
| Sun, 18 May 2008 15:04:09 +0200 |
wenzelm |
moved global pretty/string_of functions from Sign to Syntax;
|
file |
diff |
annotate
|
| Wed, 19 Mar 2008 07:20:32 +0100 |
haftmann |
Type.lookup now curried
|
file |
diff |
annotate
|
| Tue, 07 Aug 2007 20:19:55 +0200 |
wenzelm |
turned Unify flags into configuration options (global only);
|
file |
diff |
annotate
|
| Thu, 31 May 2007 23:47:36 +0200 |
wenzelm |
simplified/unified list fold;
|
file |
diff |
annotate
|
| Thu, 21 Sep 2006 19:04:20 +0200 |
wenzelm |
member (op =);
|
file |
diff |
annotate
|
| Fri, 15 Sep 2006 22:56:13 +0200 |
wenzelm |
renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
|
file |
diff |
annotate
|
| Tue, 11 Jul 2006 23:00:35 +0200 |
wenzelm |
removed obsolete xless;
|
file |
diff |
annotate
|
| Tue, 11 Jul 2006 12:17:08 +0200 |
wenzelm |
removed obsolete mem_ix;
|
file |
diff |
annotate
|
| Thu, 06 Jul 2006 11:26:46 +0200 |
wenzelm |
matchers: fall back on plain first_order_matchers, not pattern;
|
file |
diff |
annotate
|
| Mon, 19 Jun 2006 17:19:04 +0200 |
wenzelm |
matchers: try pattern_matchers only *after* general matching (The
|
file |
diff |
annotate
|
| Tue, 13 Jun 2006 23:41:39 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 12 Jun 2006 21:19:06 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 12 Jun 2006 21:19:04 +0200 |
wenzelm |
added matchers, matches_list;
|
file |
diff |
annotate
|
| Wed, 26 Apr 2006 22:38:05 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 06 Feb 2006 20:59:42 +0100 |
wenzelm |
moved combound, rlist_abs to logic.ML;
|
file |
diff |
annotate
|
| Wed, 16 Nov 2005 17:45:30 +0100 |
wenzelm |
tuned Pattern.match/unify;
|
file |
diff |
annotate
|
| Tue, 13 Sep 2005 22:19:28 +0200 |
wenzelm |
Seq.maps;
|
file |
diff |
annotate
|
| Thu, 28 Jul 2005 15:19:49 +0200 |
wenzelm |
Sign.typ_unify;
|
file |
diff |
annotate
|
| Fri, 01 Jul 2005 22:29:19 +0200 |
wenzelm |
back to 1.28;
|
file |
diff |
annotate
|
| Thu, 30 Jun 2005 19:49:41 +0200 |
wenzelm |
revert to 1.27 due to obscure performance issues (!??);
|
file |
diff |
annotate
|
| Wed, 29 Jun 2005 15:13:32 +0200 |
wenzelm |
pass thy as explicit argument (the old ref was not safe
|
file |
diff |
annotate
|
| Fri, 17 Jun 2005 18:33:08 +0200 |
wenzelm |
accomodate identification of type Sign.sg and theory;
|
file |
diff |
annotate
|
| Thu, 21 Apr 2005 19:12:03 +0200 |
berghofe |
- Eliminated nodup_vars check.
|
file |
diff |
annotate
|
| Fri, 04 Mar 2005 15:07:34 +0100 |
skalberg |
Removed practically all references to Library.foldr.
|
file |
diff |
annotate
|
| Thu, 03 Mar 2005 12:43:01 +0100 |
skalberg |
Move towards standard functions.
|
file |
diff |
annotate
|
| Sun, 13 Feb 2005 17:15:14 +0100 |
skalberg |
Deleted Library.option type.
|
file |
diff |
annotate
|
| Thu, 11 Nov 2004 10:26:40 +0100 |
paulson |
increased tracing and search bounds
|
file |
diff |
annotate
|
| Thu, 22 Apr 2004 10:52:32 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 18 Dec 2001 02:17:20 +0100 |
wenzelm |
tuned Type.unify;
|
file |
diff |
annotate
|
| Wed, 21 Nov 2001 00:36:51 +0100 |
wenzelm |
use tracing function for trace output;
|
file |
diff |
annotate
|
| Mon, 19 Nov 2001 17:32:49 +0100 |
berghofe |
Moved head_norm and fastype from unify.ML to envir.ML
|
file |
diff |
annotate
|
| Fri, 10 Mar 2000 14:57:06 +0100 |
berghofe |
Type.unify and Type.typ_match now use Vartab instead of association lists.
|
file |
diff |
annotate
|
| Fri, 19 Dec 1997 09:58:03 +0100 |
wenzelm |
adapted to new sort function;
|
file |
diff |
annotate
|
| Thu, 27 Nov 1997 19:36:31 +0100 |
wenzelm |
fixed warning;
|
file |
diff |
annotate
|
| Fri, 21 Nov 1997 15:27:43 +0100 |
wenzelm |
changed Sequence interface (now Seq, in seq.ML);
|
file |
diff |
annotate
|
| Fri, 24 Oct 1997 17:13:21 +0200 |
wenzelm |
ProtoPure.thy;
|
file |
diff |
annotate
|
| Fri, 07 Mar 1997 10:26:02 +0100 |
paulson |
Removed some polymorphic equality tests
|
file |
diff |
annotate
|
| Mon, 18 Nov 1996 16:30:06 +0100 |
paulson |
Changed subst_bounds to subst_bound, to run faster
|
file |
diff |
annotate
|
| Tue, 12 Nov 1996 11:57:10 +0100 |
paulson |
Changed some mem calls to be monomorphic
|
file |
diff |
annotate
|
| Wed, 30 Oct 1996 11:21:24 +0100 |
paulson |
Changed some mem calls to mem_int for greater efficiency (not that it could matter)
|
file |
diff |
annotate
|
| Fri, 16 Feb 1996 13:55:29 +0100 |
paulson |
Elimination of fully-functorial style.
|
file |
diff |
annotate
|
| Mon, 29 Jan 1996 14:16:13 +0100 |
clasohm |
inserted tabs again
|
file |
diff |
annotate
|
| Mon, 29 Jan 1996 13:56:41 +0100 |
clasohm |
removed tabs
|
file |
diff |
annotate
|
| Thu, 11 Jan 1996 10:29:31 +0100 |
nipkow |
Removed bug in type unification. Negative indexes are not used any longer.
|
file |
diff |
annotate
|
| Fri, 03 Mar 1995 11:48:05 +0100 |
clasohm |
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
|
file |
diff |
annotate
|
| Fri, 21 Oct 1994 09:53:38 +0100 |
lcp |
Pure/Unify/IMPROVING "CLEANING" OF FLEX-FLEX PAIRS: Old code would refuse
|
file |
diff |
annotate
|
| Wed, 19 Oct 1994 09:48:13 +0100 |
lcp |
new comments explaining abandoned change
|
file |
diff |
annotate
|
| Thu, 16 Sep 1993 12:20:38 +0200 |
clasohm |
Initial revision
|
file |
diff |
annotate
|