| #
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
|