History log of /seL4-l4v-master/isabelle/src/Pure/net.ML
Revision Date Author Comments
# 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