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