src/Provers/Arith/combine_numerals.ML
Tue, 13 Aug 2019 21:52:08 +0200 wenzelm tuned;
Tue, 04 Jun 2019 20:49:33 +0200 wenzelm tuned;
Tue, 04 Jun 2019 13:09:24 +0200 wenzelm proper context;
Wed, 09 Sep 2015 20:57:21 +0200 wenzelm simplified simproc programming interfaces;
Wed, 11 Feb 2015 11:18:36 +0100 wenzelm proper context;
Tue, 10 Feb 2015 14:48:26 +0100 wenzelm proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
Thu, 30 Oct 2014 16:55:29 +0100 wenzelm eliminated aliases;
Thu, 18 Apr 2013 17:07:01 +0200 wenzelm simplifier uses proper Proof.context instead of historic type simpset;
Sat, 17 Sep 2011 15:08:55 +0200 haftmann dropped unused argument – avoids problem with SML/NJ
Sat, 13 Mar 2010 16:44:12 +0100 wenzelm removed old CVS Ids;
Mon, 21 May 2007 19:05:37 +0200 huffman generalize CombineNumerals functor to allow coefficients with types other than IntInf.int
Wed, 12 Jul 2006 21:19:17 +0200 wenzelm prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
Sat, 08 Jul 2006 12:54:30 +0200 wenzelm simprocs: no theory argument -- use simpset context instead;
Thu, 15 Sep 2005 17:16:56 +0200 wenzelm TableFun/Symtab: curried lookup and update;
Thu, 01 Sep 2005 22:15:12 +0200 wenzelm curried_lookup/update;
less more (0) -15 tip