#
f6c05490 |
|
05-Aug-2016 |
wenzelm <none@none> |
tuned;
|
#
90b5dde1 |
|
12-Mar-2014 |
wenzelm <none@none> |
minor tuning -- NB: props are usually empty for global facts;
|
#
c686572c |
|
24-Feb-2014 |
wenzelm <none@none> |
optimize special case according to Library.merge (see also 8fbc355100f2); no treatment for Net.merge, due to non-standard merge order;
|
#
e3d2537f |
|
08-Nov-2011 |
wenzelm <none@none> |
tuned;
|
#
dcdb2a24 |
|
24-Jun-2010 |
wenzelm <none@none> |
Net.encode_type;
|
#
bc3c5d4c |
|
01-Nov-2009 |
wenzelm <none@none> |
added insert_safe, delete_safe variants;
|
#
1bd59ac7 |
|
21-Jan-2009 |
wenzelm <none@none> |
removed Ids;
|
#
ca14c530 |
|
31-May-2007 |
wenzelm <none@none> |
simplified/unified list fold;
|
#
2b2592c0 |
|
10-Jul-2006 |
wenzelm <none@none> |
Name.bound;
|
#
28432215 |
|
04-Jul-2006 |
wenzelm <none@none> |
added content;
|
#
cf09f0e2 |
|
27-Apr-2006 |
wenzelm <none@none> |
tuned basic list operators (flat, maps, map_filter);
|
#
dbf860ba |
|
06-Feb-2006 |
wenzelm <none@none> |
tuned;
|
#
45dec154 |
|
15-Sep-2005 |
wenzelm <none@none> |
TableFun/Symtab: curried lookup and update;
|
#
c968ef97 |
|
01-Sep-2005 |
wenzelm <none@none> |
curried_lookup/update;
|
#
b759b29c |
|
01-Aug-2005 |
wenzelm <none@none> |
nameless Term.bound;
|
#
d2e2089d |
|
28-Jul-2005 |
wenzelm <none@none> |
Term.bound;
|
#
1dbd51e6 |
|
14-Jul-2005 |
wenzelm <none@none> |
tuned;
|
#
8662082a |
|
13-Jul-2005 |
wenzelm <none@none> |
added subtract; improved interface; tuned;
|
#
29b4e88b |
|
06-Jul-2005 |
wenzelm <none@none> |
removed timers;
|
#
6966105e |
|
06-Jul-2005 |
wenzelm <none@none> |
use Symtab.table instead of ordered lists;
|
#
e6565681 |
|
05-Jul-2005 |
wenzelm <none@none> |
tuned;
|
#
2ede313a |
|
04-Jul-2005 |
wenzelm <none@none> |
use fast_string_ord;
|
#
9cc62485 |
|
04-Mar-2005 |
skalberg <none@none> |
Removed practically all references to Library.foldr.
|
#
eee46a1e |
|
02-Mar-2005 |
skalberg <none@none> |
Move towards standard functions.
|
#
850367d9 |
|
28-Nov-2001 |
wenzelm <none@none> |
most general type of delete/delete_term;
|
#
186f4da4 |
|
27-Oct-1999 |
oheimb <none@none> |
now more than 256 generated bound variables possible
|
#
3ab70f1a |
|
29-Apr-1999 |
nipkow <none@none> |
Eta contraction is now performed all the time during rewriting.
|
#
34a5a33d |
|
23-Jul-1997 |
wenzelm <none@none> |
fixed polymorphic val;
|
#
1e1a075d |
|
22-Jul-1997 |
wenzelm <none@none> |
tuned title;
|
#
7cc2e1c2 |
|
22-Jul-1997 |
wenzelm <none@none> |
added dest and merge operations;
|
#
56ec69eb |
|
25-Mar-1997 |
paulson <none@none> |
Toby's better treatment of eta-contraction
|
#
4d798205 |
|
14-Mar-1997 |
nipkow <none@none> |
Avoid eta-contraction in the simplifier. Instead the net needs to eta-contract the object. Also added a special function loose_bvar1(i,t) in term.ML.
|
#
d42856da |
|
21-Feb-1997 |
paulson <none@none> |
Replaced "flat" by the Basis Library function List.concat
|
#
9a07d392 |
|
26-Nov-1996 |
paulson <none@none> |
Eta-expansion of a function definition, for value polymorphism
|
#
f54858a0 |
|
15-Feb-1996 |
paulson <none@none> |
Elimination of fully-functorial style. Type tactic changed to a type abbrevation (from a datatype). Constructor tactic and function apply deleted.
|
#
ecb6e3c2 |
|
29-Jan-1996 |
clasohm <none@none> |
inserted tabs again
|
#
385672e0 |
|
29-Jan-1996 |
clasohm <none@none> |
removed tabs
|
#
64d0f0eb |
|
17-Jan-1994 |
nipkow <none@none> |
some optimizations of Larry's
|
#
a0f6f37f |
|
14-Jan-1994 |
nipkow <none@none> |
optimized net for matching of abstractions to speed up simplifier
|
#
f253ef6a |
|
15-Sep-1993 |
clasohm <none@none> |
Initial revision
|