| 2001-10-24 |
wenzelm |
2001-10-24 |
added lambda;
|
file | diff | annotate |
| 2001-10-23 |
wenzelm |
2001-10-23 |
replace_dummy_patterns: lift over bounds;
|
file | diff | annotate |
| 2001-05-31 |
wenzelm |
2001-05-31 |
invent_names
|
file | diff | annotate |
| 2001-01-06 |
wenzelm |
2001-01-06 |
added list_abs;
|
file | diff | annotate |
| 2000-12-13 |
wenzelm |
2000-12-13 |
fixed add_term_names: NameSpace.base;
|
file | diff | annotate |
| 2000-11-30 |
wenzelm |
2000-11-30 |
added is_replaced_dummy_pattern;
|
file | diff | annotate |
| 2000-08-29 |
nipkow |
2000-08-29 |
*** empty log message ***
|
file | diff | annotate |
| 2000-08-04 |
wenzelm |
2000-08-04 |
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
|
file | diff | annotate |
| 2000-07-13 |
wenzelm |
2000-07-13 |
add_term_consts: ins_string;
|
file | diff | annotate |
| 2000-03-30 |
wenzelm |
2000-03-30 |
foldl_term_types: depend on term as well;
|
file | diff | annotate |
| 2000-03-10 |
berghofe |
2000-03-10 |
Added functions subst_TVars_Vartab and typ_subst_TVars_Vartab.
|
file | diff | annotate |
| 1999-09-29 |
wenzelm |
1999-09-29 |
added rems_sort;
|
file | diff | annotate |
| 1999-09-01 |
wenzelm |
1999-09-01 |
structure Termtab;
|
file | diff | annotate |
| 1999-08-23 |
nipkow |
1999-08-23 |
Corrected two busg in the simplifier.
|
file | diff | annotate |
| 1999-07-10 |
wenzelm |
1999-07-10 |
Symtab.lookup_multi;
|
file | diff | annotate |
| 1999-04-30 |
wenzelm |
1999-04-30 |
val foldl_map_aterms: ('a * term -> 'a * term) -> 'a * term -> 'a * term;
|
file | diff | annotate |
| 1998-12-18 |
paulson |
1998-12-18 |
moved dest_Type to term.ML from HOL/Tools/primrec_package
|
file | diff | annotate |
| 1998-11-29 |
wenzelm |
1998-11-29 |
added oct_char;
|
file | diff | annotate |
| 1998-09-29 |
paulson |
1998-09-29 |
new function inter_term
|
file | diff | annotate |
| 1998-03-09 |
wenzelm |
1998-03-09 |
tuned some names;
|
file | diff | annotate |
| 1998-02-18 |
nipkow |
1998-02-18 |
Improved loop-test for rewrite rules a little.
Should be done properly!
|
file | diff | annotate |
| 1998-02-12 |
wenzelm |
1998-02-12 |
tuned comments;
|
file | diff | annotate |
| 1998-02-06 |
wenzelm |
1998-02-06 |
added Vartab: TABLE;
|
file | diff | annotate |
| 1997-12-28 |
wenzelm |
1997-12-28 |
made MLWorks happy;
|
file | diff | annotate |
| 1997-12-28 |
wenzelm |
1997-12-28 |
renamed Symtab.null to Symtab.empty;
|
file | diff | annotate |
| 1997-12-24 |
wenzelm |
1997-12-24 |
export range_type;
|
file | diff | annotate |
| 1997-12-22 |
paulson |
1997-12-22 |
Added range-type for completeness
|
file | diff | annotate |
| 1997-12-19 |
wenzelm |
1997-12-19 |
term order;
signature;
|
file | diff | annotate |
| 1997-11-26 |
wenzelm |
1997-11-26 |
added foldl_atyps: ('a * typ -> 'a) -> 'a * typ -> 'a;
added foldl_aterms: ('a * term -> 'a) -> 'a * term -> 'a;
added foldl_types: ('a * typ -> 'a) -> 'a * term -> 'a;
|
file | diff | annotate |
| 1997-11-07 |
oheimb |
1997-11-07 |
changed libraray function find to find_index_eq, currying it
|
file | diff | annotate |
| 1997-11-07 |
oheimb |
1997-11-07 |
added exists_Const
|
file | diff | annotate |
| 1997-11-01 |
paulson |
1997-11-01 |
New syntax function for types
|
file | diff | annotate |
| 1997-10-28 |
wenzelm |
1997-10-28 |
add_typ_classes, add_typ_tycons, add_term_classes, add_term_tycons,
add_term_consts, map_typ, map_term: moved from sign.ML to term.ML;
|
file | diff | annotate |
| 1997-10-21 |
wenzelm |
1997-10-21 |
made Poly/ML happy, but SML/NJ unhappy;
|
file | diff | annotate |
| 1997-10-20 |
wenzelm |
1997-10-20 |
make SML/NJ happy;
|
file | diff | annotate |
| 1997-10-06 |
wenzelm |
1997-10-06 |
eliminated raise_term;
|
file | diff | annotate |
| 1997-04-16 |
wenzelm |
1997-04-16 |
tuned type of eq_ix, mem_ix;
|
file | diff | annotate |
| 1997-03-14 |
nipkow |
1997-03-14 |
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.
|
file | diff | annotate |
| 1997-03-07 |
paulson |
1997-03-07 |
Improved indentation of aconv
|
file | diff | annotate |
| 1997-02-04 |
paulson |
1997-02-04 |
Gradual switching to Basis Library functions nth, drop, etc.
|
file | diff | annotate |
| 1996-11-18 |
paulson |
1996-11-18 |
Optimizations: removal of polymorphic equality; one-argument case
for subst_bounds
|
file | diff | annotate |
| 1996-11-13 |
paulson |
1996-11-13 |
Removal of polymorphic equality via mem, subset, eq_set, etc
|
file | diff | annotate |
| 1996-11-12 |
paulson |
1996-11-12 |
Changed some mem and ins calls to be monomorphic
|
file | diff | annotate |
| 1996-11-01 |
paulson |
1996-11-01 |
maxidx_of_typs replaces max o map maxidx_of_typ
Now uses Int.max instead of max
|
file | diff | annotate |
| 1996-10-30 |
paulson |
1996-10-30 |
Changed some mem calls to mem_string for greater efficiency (not that it could matter)
|
file | diff | annotate |
| 1996-01-29 |
clasohm |
1996-01-29 |
inserted tabs again
|
file | diff | annotate |
| 1996-01-29 |
clasohm |
1996-01-29 |
removed tabs
|
file | diff | annotate |
| 1995-12-28 |
paulson |
1995-12-28 |
Updated comments for compression functions
|
file | diff | annotate |
| 1995-12-22 |
paulson |
1995-12-22 |
Addition of compression, that is, sharing.
Uses refs and Symtab (binary search trees) to get reasonable speed.
Types and terms can be compressed.
|
file | diff | annotate |
| 1995-12-08 |
paulson |
1995-12-08 |
type_of1: improved error messages
|
file | diff | annotate |
| 1995-11-23 |
clasohm |
1995-11-23 |
files now define a structure to allow SML/NJ to optimize the code
|
file | diff | annotate |
| 1995-04-12 |
nipkow |
1995-04-12 |
term.ML: add_loose_bnos now returns a list w/o duplicates.
pattern.ML: replaced null(loose_bnos t) by loose_bvar(t,0)
|
file | diff | annotate |
| 1995-03-13 |
nipkow |
1995-03-13 |
Changed treatment of during type inference internally generated type
variables.
1. They are renamed to 'a, 'b, 'c etc away from a given set of used names.
2. They are either frozen (turned into TFrees) or left schematic (TVars)
depending on a parameter. In goals they are frozen, for instantiations they
are left schematic.
|
file | diff | annotate |
| 1994-11-22 |
lcp |
1994-11-22 |
Pure/term: commented typ_subst_TVars, subst_TVars, subst_Vars, subst_vars
|
file | diff | annotate |
| 1994-05-18 |
wenzelm |
1994-05-18 |
added logicC: class, logicS: sort;
added itselfT: typ -> typ, a_itselfT: typ (for axclasses);
|
file | diff | annotate |
| 1993-10-21 |
lcp |
1993-10-21 |
Pure/term/fastype_of1: renamed from fastype_of
Pure/term/fastype_of: new, takes only one argument (like type_of)
Pure/Syntax/printer/is_prop: now calls fastype_of1
Pure/pattern: now calls new fastype_of in three places
Pure/logic/mk_equals,mk_flexpair: now calls fastype_of instead of type_of.
So it no longer checks t properly -- but it never checked u anyway, and all
existing calls are derived from certified terms...
|
file | diff | annotate |
| 1993-10-08 |
wenzelm |
1993-10-08 |
added raise_type: string -> typ list -> term list -> 'a;
added raise_term: string -> term list -> 'a;
|
file | diff | annotate |
| 1993-09-16 |
clasohm |
1993-09-16 |
Initial revision
|
file | diff | annotate |