#
294413f4 |
|
13-Aug-2019 |
wenzelm <none@none> |
tuned;
|
#
e3aa1038 |
|
04-Jun-2019 |
wenzelm <none@none> |
tuned;
|
#
cb36e51e |
|
04-Jun-2019 |
wenzelm <none@none> |
proper context;
|
#
e0a30cbb |
|
09-Sep-2015 |
wenzelm <none@none> |
simplified simproc programming interfaces;
|
#
eeb00f20 |
|
11-Feb-2015 |
wenzelm <none@none> |
proper context; tuned whitespace;
|
#
b8d56fe6 |
|
10-Feb-2015 |
wenzelm <none@none> |
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; occasionally clarified use of context;
|
#
2d556eb3 |
|
30-Oct-2014 |
wenzelm <none@none> |
eliminated aliases;
|
#
0928b2db |
|
18-Apr-2013 |
wenzelm <none@none> |
simplifier uses proper Proof.context instead of historic type simpset;
|
#
527a4060 |
|
17-Sep-2011 |
haftmann <none@none> |
dropped unused argument – avoids problem with SML/NJ
|
#
458a4961 |
|
13-Mar-2010 |
wenzelm <none@none> |
removed old CVS Ids; tuned headers;
|
#
e31c6f0b |
|
21-May-2007 |
huffman <none@none> |
generalize CombineNumerals functor to allow coefficients with types other than IntInf.int
|
#
99f1dcf9 |
|
12-Jul-2006 |
wenzelm <none@none> |
prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars; tuned;
|
#
cfdc1311 |
|
07-Jul-2006 |
wenzelm <none@none> |
simprocs: no theory argument -- use simpset context instead;
|
#
45dec154 |
|
15-Sep-2005 |
wenzelm <none@none> |
TableFun/Symtab: curried lookup and update;
|
#
8d88d1ec |
|
01-Sep-2005 |
wenzelm <none@none> |
curried_lookup/update;
|
#
678cd7d2 |
|
01-Aug-2005 |
wenzelm <none@none> |
simprocs: Simplifier.inherit_bounds;
|
#
f2340401 |
|
16-May-2005 |
paulson <none@none> |
Use of IntInf.int instead of int in most numeric simprocs; avoids integer overflow in SML/NJ
|
#
eee46a1e |
|
02-Mar-2005 |
skalberg <none@none> |
Move towards standard functions.
|
#
3dffd254 |
|
13-Feb-2005 |
skalberg <none@none> |
Deleted Library.option type.
|
#
69fd4979 |
|
08-Jul-2004 |
wenzelm <none@none> |
adapted type of simprocs;
|
#
d464418c |
|
15-Feb-2004 |
paulson <none@none> |
Polymorphic treatment of binary arithmetic using axclasses
|
#
d5d4b801 |
|
08-Aug-2002 |
wenzelm <none@none> |
adhoc_freeze_vars;
|
#
1f3db197 |
|
17-Aug-2000 |
paulson <none@none> |
now allows dest_coeff to fail
|
#
d48bc018 |
|
10-Aug-2000 |
paulson <none@none> |
new structure field "add" for CombineNumerals
|
#
169454c1 |
|
29-Jun-2000 |
paulson <none@none> |
now freezes Vars in order to prevent errors in cases like these: Goal "Suc (x + i + j) + ?q ?ii ?jj + k + x = xxx"; Goal "Suc (x + i + j) = x + f(?q i j) + k"; Goal "Suc (x + i + j) = x + ?q i j + k"; Goal "Suc (?q ?ii ?jj + i + j) + ?rq ?ii ?jj + k + ?q ?ii ?jj = xxx";
|
#
c943e92b |
|
05-May-2000 |
wenzelm <none@none> |
removed dead code: listof;
|
#
27e5e19d |
|
05-May-2000 |
paulson <none@none> |
simprocs now simplify the RHS of their result
|
#
41314fd2 |
|
02-May-2000 |
paulson <none@none> |
new simproc, replacing combine_coeffs and working for nat, int, real
|