src/Provers/Arith/extract_common_term.ML
2013-04-18 wenzelm simplifier uses proper Proof.context instead of historic type simpset;
2011-10-29 huffman remove unused function
2011-10-27 huffman 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
2011-06-29 wenzelm tuned signature;
2010-03-13 wenzelm removed old CVS Ids;
2009-03-22 nipkow 1. New cancellation simprocs for common factors in inequations
2006-07-12 wenzelm prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
2006-07-08 wenzelm simprocs: no theory argument -- use simpset context instead;
2005-09-15 wenzelm TableFun/Symtab: curried lookup and update;
2005-09-01 wenzelm curried_lookup/update;
2005-08-01 wenzelm simprocs: Simplifier.inherit_bounds;
2005-03-03 skalberg Move towards standard functions.
2005-02-13 skalberg Deleted Library.option type.
2004-07-08 wenzelm adapted type of simprocs;
2004-02-15 paulson Polymorphic treatment of binary arithmetic using axclasses
2002-08-08 wenzelm adhoc_freeze_vars;
2000-12-18 paulson new simproc for cancelling common factors, etc.
less more (0) tip