src/Provers/Arith/assoc_fold.ML
Sat, 18 Jul 2015 20:54:56 +0200 wenzelm prefer tactics with explicit context;
Thu, 18 Apr 2013 17:07:01 +0200 wenzelm simplifier uses proper Proof.context instead of historic type simpset;
Sat, 13 Mar 2010 16:44:12 +0100 wenzelm removed old CVS Ids;
Thu, 26 Mar 2009 11:33:50 -0700 huffman parameterize assoc_fold with is_numeral predicate
Tue, 15 Jan 2008 16:19:23 +0100 haftmann joined theories IntDef, Numeral, IntArith to theory Int
Thu, 17 May 2007 19:49:40 +0200 haftmann canonical prefixing of class constants
Sat, 08 Jul 2006 12:54:43 +0200 wenzelm simprocs: no theory argument -- use simpset context instead;
Fri, 21 Oct 2005 18:14:34 +0200 wenzelm Goal.prove;
Mon, 17 Oct 2005 23:10:15 +0200 wenzelm Simplifier.inherit_context instead of Simplifier.inherit_bounds;
Mon, 01 Aug 2005 19:20:26 +0200 wenzelm simprocs: Simplifier.inherit_bounds;
Fri, 17 Jun 2005 18:33:03 +0200 wenzelm renamed sg_ref to thy_ref;
Sun, 13 Feb 2005 17:15:14 +0100 skalberg Deleted Library.option type.
Sun, 15 Feb 2004 10:46:37 +0100 paulson Polymorphic treatment of binary arithmetic using axclasses
Thu, 08 Aug 2002 23:46:09 +0200 wenzelm use Tactic.prove instead of prove_goalw_cterm in internal proofs!
Tue, 06 Aug 2002 11:22:05 +0200 wenzelm sane interface for simprocs;
Wed, 21 Nov 2001 00:36:51 +0100 wenzelm use tracing function for trace output;
Mon, 24 Jul 2000 23:47:57 +0200 wenzelm do not pass theory values, but sg_ref;
Tue, 30 May 2000 16:03:09 +0200 wenzelm global timing flag;
Fri, 12 May 2000 11:52:44 +0200 wenzelm improved name of simproc;
Fri, 23 Jul 1999 17:24:48 +0200 paulson new simprocs assoc_fold and combine_coeff
less more (0) tip