src/HOL/Tools/Qelim/presburger.ML
Thu, 29 May 2008 23:46:40 +0200 wenzelm proper context for ss;
Sat, 05 Jan 2008 23:05:29 +0100 chaieb Tuned relevant premises selection
Thu, 03 Jan 2008 18:19:27 +0100 chaieb tuned relevance test for presburger
Thu, 03 Jan 2008 10:27:34 +0100 chaieb Changed order of tactics in presburger --- thinning before case splits
Wed, 02 Jan 2008 15:14:24 +0100 haftmann some more antiquotations
Fri, 12 Oct 2007 08:25:48 +0200 haftmann moved class power to theory Power
Sat, 15 Sep 2007 19:27:35 +0200 haftmann fixed title
Wed, 22 Aug 2007 17:13:41 +0200 chaieb More selective generalization : a*b is generalized whenever none of a and b is a number
Fri, 20 Jul 2007 14:28:05 +0200 haftmann dropped Nat.ML legacy bindings
Tue, 03 Jul 2007 17:17:04 +0200 wenzelm CONVERSION tactical;
Mon, 25 Jun 2007 22:46:55 +0200 wenzelm tactics: more robust addressing of subgoal using (C)SUBGOAL/THEN_ALL_NEW;
Mon, 25 Jun 2007 00:36:37 +0200 wenzelm Thm.eta_long_conversion;
Thu, 21 Jun 2007 22:52:22 +0200 huffman add thm antiquotations
Thu, 21 Jun 2007 20:48:48 +0200 wenzelm moved quantifier elimination tools to Tools/Qelim/;
less more (0) tip