| #
e3aa1038 |
|
04-Jun-2019 |
wenzelm <none@none> |
tuned;
|
| #
cb36e51e |
|
04-Jun-2019 |
wenzelm <none@none> |
proper context;
|
| #
0928b2db |
|
18-Apr-2013 |
wenzelm <none@none> |
simplifier uses proper Proof.context instead of historic type simpset;
|
| #
b29cf7a3 |
|
29-Oct-2011 |
huffman <none@none> |
remove unused function
|
| #
64e2fca3 |
|
26-Oct-2011 |
huffman <none@none> |
fix bug in cancel_factor simprocs so they will work on goals like 'x * y < x * z' where the common term is already on the left
|
| #
a9de3adb |
|
29-Jun-2011 |
wenzelm <none@none> |
tuned signature;
|
| #
458a4961 |
|
13-Mar-2010 |
wenzelm <none@none> |
removed old CVS Ids;
tuned headers;
|
| #
3139985e |
|
22-Mar-2009 |
nipkow <none@none> |
1. New cancellation simprocs for common factors in inequations
2. Updated the documentation
|
| #
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;
|
| #
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;
|
| #
81040be0 |
|
18-Dec-2000 |
paulson <none@none> |
new simproc for cancelling common factors, etc.
|