#
90e0a6db |
|
30-Jul-2019 |
wenzelm <none@none> |
clarified modules;
|
#
0e5c06bc |
|
03-Jan-2019 |
wenzelm <none@none> |
clarified signature: more types;
|
#
401e509b |
|
13-Dec-2016 |
wenzelm <none@none> |
more symbols;
|
#
5e705c5a |
|
19-Aug-2016 |
nipkow <none@none> |
replaced the confusing int parameter by bool
|
#
0bca046a |
|
21-Nov-2014 |
wenzelm <none@none> |
removed some add-ons from modules that are relevant for the inference kernel;
|
#
16b4f761 |
|
08-Nov-2014 |
wenzelm <none@none> |
optional proof context for unify operations, for the sake of proper local options;
|
#
fcc41d2e |
|
01-Nov-2014 |
wenzelm <none@none> |
eliminated former Proof General preferences;
|
#
bced7572 |
|
06-Apr-2014 |
wenzelm <none@none> |
more source positions;
|
#
48675c42 |
|
19-Jul-2013 |
wenzelm <none@none> |
turned pattern unify flag into configuration option (global only);
|
#
e4d829b0 |
|
29-May-2013 |
wenzelm <none@none> |
backout 3b9c31867707 -- too risky to "amend" modules from 25 years ago that don't handle Vars with different types;
|
#
52ef5040 |
|
27-May-2013 |
wenzelm <none@none> |
more thorough type unification: treat equal Vars like other atoms, otherwise unify type of term pair (not just accidental body_type of its head Vars);
|
#
0cd2a86c |
|
24-May-2013 |
wenzelm <none@none> |
proper internal error, not user error;
|
#
e712bb09 |
|
24-May-2013 |
wenzelm <none@none> |
tuned signature;
|
#
71c1f7c5 |
|
24-May-2013 |
wenzelm <none@none> |
tuned;
|
#
fa313ab9 |
|
24-May-2013 |
wenzelm <none@none> |
unify types of bound variables in the same manner as Unify.new_dpair (which emphatically "Tries to unify types of the bound variables!");
|
#
e4af045c |
|
24-May-2013 |
wenzelm <none@none> |
re-use Pattern.unify_types, including its trace_unify_fail option;
|
#
cba98832 |
|
12-Apr-2013 |
wenzelm <none@none> |
tuned signature; tuned comments;
|
#
996c1407 |
|
10-Mar-2012 |
wenzelm <none@none> |
clarified Pattern.matchess;
|
#
cfb69d7d |
|
14-Jan-2012 |
wenzelm <none@none> |
discontinued old-style Term.list_abs in favour of plain Term.abs;
|
#
6701cdc1 |
|
24-Mar-2011 |
wenzelm <none@none> |
added Term.is_open and Term.is_dependent convenience, to cover common situations of loose bounds;
|
#
78338fa3 |
|
07-Dec-2010 |
wenzelm <none@none> |
eliminated some hard tabulators (deprecated);
|
#
637fe2f1 |
|
26-Nov-2010 |
wenzelm <none@none> |
make two copies (!) of Library.UnequalLengths coincide with ListPair.UnequalLengths;
|
#
a76d8de4 |
|
19-Nov-2010 |
paulson <none@none> |
First-order pattern matching: catch a rogue exception (differing numbers of arguments)
|
#
e3d0611a |
|
27-Feb-2010 |
wenzelm <none@none> |
modernized structure Term_Ord;
|
#
67bd785b |
|
18-Feb-2010 |
berghofe <none@none> |
Added function rewrite_term_top for top-down rewriting.
|
#
8eb709ab |
|
20-Oct-2009 |
haftmann <none@none> |
curried inter as canonical list operation (beware of argument order)
|
#
8de45ab6 |
|
21-Oct-2009 |
haftmann <none@none> |
dropped redundant gen_ prefix
|
#
68478f6d |
|
20-Oct-2009 |
haftmann <none@none> |
replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
|
#
b9d789f1 |
|
29-Sep-2009 |
wenzelm <none@none> |
explicit indication of Unsynchronized.ref;
|
#
d9aef710 |
|
17-Jul-2009 |
wenzelm <none@none> |
tuned/modernized Envir.subst_XXX;
|
#
e895af14 |
|
17-Jul-2009 |
wenzelm <none@none> |
tuned/modernized Envir operations;
|
#
e77d98cf |
|
17-Mar-2009 |
wenzelm <none@none> |
export match_rew -- useful for implementing "procs" for rewrite_term;
|
#
a3d0c258 |
|
16-Mar-2009 |
wenzelm <none@none> |
tuned aeconv: test plain aconv before expensive eta_contract;
|
#
e154e805 |
|
31-Dec-2008 |
wenzelm <none@none> |
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML); tuned signature of structure Term;
|
#
e777200f |
|
25-Sep-2008 |
haftmann <none@none> |
matchess
|
#
70a4fc69 |
|
18-May-2008 |
wenzelm <none@none> |
moved global pretty/string_of functions from Sign to Syntax;
|
#
09e90ee9 |
|
07-May-2008 |
berghofe <none@none> |
- Removed function eta_contract_atom, which did not quite work - Corrected and simplified function aeconv
|
#
e2e9e591 |
|
27-Nov-2007 |
berghofe <none@none> |
first_order_match now only calls loose_bvar when inside an abstraction.
|
#
40430774 |
|
03-Jun-2007 |
wenzelm <none@none> |
added downto0 (from library.ML);
|
#
ed851154 |
|
14-Apr-2007 |
wenzelm <none@none> |
Term.string_of_vname;
|
#
8d1a7e60 |
|
06-Feb-2007 |
wenzelm <none@none> |
tuned matches_subterm;
|
#
5d0e41dc |
|
21-Sep-2006 |
wenzelm <none@none> |
member (op =); tuned pattern check;
|
#
49eb413f |
|
11-Jul-2006 |
wenzelm <none@none> |
removed obsolete xless;
|
#
4cebcc47 |
|
10-Jul-2006 |
wenzelm <none@none> |
replaced Term.variant(list) by Name.variant(_list); Name.bound;
|
#
59e4d6bf |
|
13-Jun-2006 |
wenzelm <none@none> |
added equiv;
|
#
677f928d |
|
12-Jun-2006 |
wenzelm <none@none> |
removed matches_seq -- didn't quite work;
|
#
f55d7533 |
|
05-Jun-2006 |
wenzelm <none@none> |
added matches_seq (left-to-right matching, intermediate beta-normalization);
|
#
44d31bf2 |
|
29-Apr-2006 |
wenzelm <none@none> |
tuned;
|
#
cf09f0e2 |
|
27-Apr-2006 |
wenzelm <none@none> |
tuned basic list operators (flat, maps, map_filter);
|
#
37f66101 |
|
20-Mar-2006 |
wenzelm <none@none> |
subtract (op =);
|
#
caba7fb7 |
|
06-Feb-2006 |
wenzelm <none@none> |
moved (beta_)eta_contract to envir.ML; tuned;
|
#
d19ae56d |
|
16-Nov-2005 |
wenzelm <none@none> |
tuned interfaces to support incremental match/unify (cf. versions in type.ML);
|
#
67bf68ad |
|
28-Oct-2005 |
haftmann <none@none> |
cleaned up nth, nth_update, nth_map and nth_string functions
|
#
db589537 |
|
04-Oct-2005 |
wenzelm <none@none> |
minor tweaks for Poplog/ML;
|
#
45dec154 |
|
15-Sep-2005 |
wenzelm <none@none> |
TableFun/Symtab: curried lookup and update;
|
#
c968ef97 |
|
01-Sep-2005 |
wenzelm <none@none> |
curried_lookup/update;
|
#
e7b1feab |
|
31-Aug-2005 |
wenzelm <none@none> |
refer to theory instead of low-level tsig;
|
#
b759b29c |
|
01-Aug-2005 |
wenzelm <none@none> |
nameless Term.bound;
|
#
411974f5 |
|
28-Jul-2005 |
wenzelm <none@none> |
Sign.typ_unify; Term.bound; tuned rewrite_term;
|
#
c3490754 |
|
01-Jul-2005 |
wenzelm <none@none> |
avoid polyeq;
|
#
c9e99f77 |
|
01-Jul-2005 |
berghofe <none@none> |
Changed interface of Envir.lookup'
|
#
e7bf4e72 |
|
21-Apr-2005 |
berghofe <none@none> |
- Eliminated nodup_vars check. - Unification and matching functions now check types of term variables / sorts of type variables when applying a substitution. - Thm.instantiate now takes (ctyp * ctyp) list instead of (indexname * ctyp) list as argument, to allow for proper instantiation of theorems containing type variables with same name but different sorts.
|
#
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.
|
#
3dffd254 |
|
13-Feb-2005 |
skalberg <none@none> |
Deleted Library.option type.
|
#
33b1b845 |
|
21-Jun-2004 |
kleing <none@none> |
Merged in license change from Isabelle2004
|
#
51e8a7c0 |
|
05-Jun-2004 |
wenzelm <none@none> |
avoid implicit arguments via refs;
|
#
87c797a4 |
|
01-Jun-2004 |
berghofe <none@none> |
Removed ~10000 hack in function idx that can lead to inconsistencies when unifying terms with a large number of abstractions.
|
#
5102e733 |
|
21-May-2004 |
wenzelm <none@none> |
adapted tsig interface;
|
#
ff29d609 |
|
22-Apr-2004 |
wenzelm <none@none> |
tuned;
|
#
68e0f0cb |
|
10-May-2003 |
berghofe <none@none> |
Added new function eta_long.
|
#
1e09077e |
|
04-Apr-2003 |
berghofe <none@none> |
type_of_G now applies type substitution before decomposing type.
|
#
ef58f7e0 |
|
10-Oct-2002 |
berghofe <none@none> |
norm_typ -> Envir.norm_type
|
#
7fffca59 |
|
10-Oct-2002 |
nipkow <none@none> |
added failure trace information to pattern unification
|
#
ab6f5707 |
|
31-May-2002 |
berghofe <none@none> |
Changes to rewrite_term: - now uses skeletons to speed up rewriting - added interface for rewriting procedures
|
#
1a57b494 |
|
28-Feb-2002 |
wenzelm <none@none> |
rewrite_term: Term.rename_abs;
|
#
ed3b1570 |
|
21-Jan-2002 |
berghofe <none@none> |
Removed timing function.
|
#
f23c5a8c |
|
18-Jan-2002 |
wenzelm <none@none> |
rewrite_term: removed rew0, so no on-the-fly eta-contraction;
|
#
5bb7108d |
|
17-Jan-2002 |
wenzelm <none@none> |
eta_contract with sharing (by berghofe); rewrite_term: proper handling of Abs cong;
|
#
edcad963 |
|
16-Jan-2002 |
wenzelm <none@none> |
added rewrite_term; tuned; GPLed;
|
#
95382828 |
|
16-Jan-2002 |
wenzelm <none@none> |
added beta_eta_contract;
|
#
21d13607 |
|
17-Dec-2001 |
wenzelm <none@none> |
tuned Type.unify;
|
#
3c9f7c93 |
|
19-Nov-2001 |
berghofe <none@none> |
Replaced devar by Envir.head_norm
|
#
aafaee53 |
|
10-Mar-2000 |
berghofe <none@none> |
Type.unify and Type.typ_match now use Vartab instead of association lists.
|
#
3ab70f1a |
|
29-Apr-1999 |
nipkow <none@none> |
Eta contraction is now performed all the time during rewriting.
|
#
aa959df4 |
|
22-Apr-1998 |
nipkow <none@none> |
Tried to speed up the rewriter by eta-contracting all patterns beforehand and by classifying each pattern as to whether it allows first-order matching.
|
#
36cc27e4 |
|
28-Feb-1998 |
nipkow <none@none> |
Tried to reorganize rewriter a little. More to be done.
|
#
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.
|
#
95206129 |
|
07-Mar-1997 |
paulson <none@none> |
Corrected aeconv and exported it
|
#
9943c2d2 |
|
05-Mar-1997 |
paulson <none@none> |
Declares eta_contract_atom; fixed comment; some tidying
|
#
04a178b0 |
|
14-Feb-1997 |
paulson <none@none> |
A bit more pattern-matching in eta_contract
|
#
78126b7e |
|
26-Nov-1996 |
paulson <none@none> |
Removal of needless function definition
|
#
79b79e6d |
|
14-Mar-1996 |
berghofe <none@none> |
Added some optimized versions of functions dealing with sets (i.e. mem, ins, eq_set etc.) which do not use the polymorphic = operator
|
#
60deb515 |
|
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
|
#
82dec180 |
|
11-Jan-1996 |
nipkow <none@none> |
Removed bug in type unification. Negative indexes are not used any longer. Had to change interface to Type.unify to pass maxidx. Thus changes in the clients.
|
#
a1dde6de |
|
12-Apr-1995 |
nipkow <none@none> |
term.ML: add_loose_bnos now returns a list w/o duplicates. pattern.ML: replaced null(loose_bnos t) by loose_bvar(t,0)
|
#
7a56034b |
|
02-Nov-1994 |
nipkow <none@none> |
Modified pattern.ML to perform proper matching of Higher-Order Patterns. Modified thm.ML to preserve bound var names during rewriting. Renamed eta_matches to matches.
|
#
8719fdcd |
|
21-Oct-1993 |
lcp <none@none> |
now calls new fastype_of in three places
|
#
f253ef6a |
|
15-Sep-1993 |
clasohm <none@none> |
Initial revision
|