#
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;
|
#
e119cdbc |
|
23-Nov-2013 |
wenzelm <none@none> |
tuned;
|
#
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
|
#
a9de3adb |
|
29-Jun-2011 |
wenzelm <none@none> |
tuned signature;
|
#
28640711 |
|
22-Apr-2011 |
wenzelm <none@none> |
tuned signature;
|
#
458a4961 |
|
13-Mar-2010 |
wenzelm <none@none> |
removed old CVS Ids; tuned headers;
|
#
2a4bde03 |
|
18-Sep-2007 |
wenzelm <none@none> |
simplified type int (eliminated IntInf.int, integer);
|
#
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;
|
#
441c9126 |
|
01-Sep-2005 |
wenzelm <none@none> |
curried_lookup/update; tuned;
|
#
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;
|
#
2e5f7fc6 |
|
07-Aug-2000 |
paulson <none@none> |
prove_conv gets an extra argument, so the ZF instantiation can use hyps
|
#
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";
|
#
27e5e19d |
|
05-May-2000 |
paulson <none@none> |
simprocs now simplify the RHS of their result
|
#
4a9a975e |
|
02-May-2000 |
paulson <none@none> |
various bug fixes
|
#
3029a1ef |
|
28-Apr-2000 |
paulson <none@none> |
inserted triviality check
|
#
a077507a |
|
21-Apr-2000 |
paulson <none@none> |
now works for coefficients, not just for numerals no longer works by subtraction, so no need for inverse_fold
|
#
a277cd39 |
|
18-Apr-2000 |
paulson <none@none> |
new simprocs for numerals of type "nat"
|