src/HOL/Tools/Qelim/cooper.ML
Fri, 27 Aug 2010 17:59:40 +0200 wenzelm more antiquotations;
Fri, 27 Aug 2010 10:56:46 +0200 haftmann formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
Thu, 26 Aug 2010 20:51:17 +0200 haftmann formerly unnamed infix impliciation now named HOL.implies
Thu, 19 Aug 2010 16:08:59 +0200 haftmann tuned quotes
Thu, 19 Aug 2010 11:02:14 +0200 haftmann use antiquotations for remaining unqualified constants in HOL
Tue, 08 Jun 2010 16:37:22 +0200 haftmann tuned quotes, antiquotations and whitespace
Tue, 25 May 2010 20:28:16 +0200 wenzelm eliminated various catch-all exception patterns, guessing at the concrete exeptions that are intended here;
Sat, 15 May 2010 21:50:05 +0200 wenzelm less pervasive names from structure Thm;
Tue, 11 May 2010 19:00:16 +0200 haftmann represent de-Bruin indices simply by position in list
Tue, 11 May 2010 18:46:03 +0200 haftmann tuned reification functions
Tue, 11 May 2010 18:31:36 +0200 haftmann tuned code; toward a tightended interface with generated code
Mon, 10 May 2010 15:33:32 +0200 haftmann tuned; dropped strange myassoc2
Mon, 10 May 2010 15:24:43 +0200 haftmann stylized COOPER exception
Mon, 10 May 2010 15:21:13 +0200 haftmann simplified oracle
Mon, 10 May 2010 15:00:53 +0200 haftmann shorten names
Mon, 10 May 2010 14:55:06 +0200 haftmann only one module fpr presburger method
Mon, 10 May 2010 14:11:50 +0200 haftmann one structure is better than three
Mon, 10 May 2010 13:58:18 +0200 haftmann less complex organization of cooper source code
Mon, 10 May 2010 12:25:49 +0200 haftmann dropped unused bindings; avoid open (documents dependency on generated code more explicitly)
Thu, 06 May 2010 19:27:51 +0200 haftmann merged
Thu, 06 May 2010 16:32:21 +0200 haftmann tuned whitespace; dropped superfluous open
Wed, 05 May 2010 18:25:34 +0200 haftmann farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
Wed, 28 Apr 2010 21:41:05 +0200 haftmann modernized structure name
Sun, 28 Feb 2010 23:51:31 +0100 wenzelm more antiquotations;
Fri, 19 Feb 2010 14:47:01 +0100 haftmann moved remaning class operations from Algebras.thy to Groups.thy
Wed, 10 Feb 2010 14:12:04 +0100 haftmann moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
Mon, 08 Feb 2010 17:12:38 +0100 haftmann renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
Thu, 28 Jan 2010 11:48:49 +0100 haftmann new theory Algebras.thy for generic algebraic structures
Wed, 21 Oct 2009 12:02:56 +0200 haftmann curried union as canonical list operation
Wed, 21 Oct 2009 08:16:25 +0200 haftmann merged
Wed, 21 Oct 2009 08:14:38 +0200 haftmann dropped redundant gen_ prefix
Tue, 20 Oct 2009 16:13:01 +0200 haftmann replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
Wed, 21 Oct 2009 00:36:12 +0200 wenzelm standardized basic operations on type option;
Mon, 19 Oct 2009 21:54:57 +0200 wenzelm uniform use of Integer.add/mult/sum/prod;
Fri, 18 Sep 2009 09:07:50 +0200 haftmann tuned const_name antiquotations
Fri, 28 Aug 2009 18:18:30 +0200 wenzelm modernized messages -- eliminated old Display.print_cterm;
Mon, 24 Aug 2009 10:44:03 +0200 boehmes stricter condition for (binary) integer relation
Tue, 28 Jul 2009 13:37:09 +0200 haftmann Set.UNIV and Set.empty are mere abbreviations for top and bot
Mon, 11 May 2009 15:57:29 +0200 haftmann qualified names for Lin_Arith tactics and simprocs
Mon, 23 Mar 2009 19:01:16 +0100 haftmann moved generic arith_tac (formerly silent_arith_tac), verbose_arith_tac (formerly arith_tac) to Arith_Data; simple_arith-tac now named linear_arith_tac
Thu, 19 Mar 2009 22:05:00 +0100 wenzelm proper spacing before ML antiquotations -- note that @ may be part of symbolic ML identifiers;
Wed, 11 Mar 2009 15:56:50 +0100 haftmann tuned funny error message
Thu, 05 Mar 2009 08:23:11 +0100 haftmann set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax
Tue, 03 Feb 2009 16:50:40 +0100 haftmann regenerated presburger code
Wed, 31 Dec 2008 00:08:13 +0100 wenzelm moved old add_term_vars, add_term_frees etc. to structure OldTerm;
Mon, 29 Sep 2008 11:46:47 +0200 wenzelm handle _ should be avoided (spurious Interrupt will spoil the game);
Thu, 18 Sep 2008 19:39:44 +0200 wenzelm simplified oracle interface;
Fri, 18 Jul 2008 18:25:53 +0200 haftmann moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
Mon, 23 Jun 2008 23:45:39 +0200 wenzelm Logic.all/mk_equals/mk_implies;
Thu, 29 May 2008 23:46:39 +0200 wenzelm proper context for simp_thms_conv;
Sat, 17 May 2008 13:54:30 +0200 wenzelm structure Display: less pervasive operations;
Wed, 02 Jan 2008 15:14:24 +0100 haftmann some more antiquotations
Tue, 18 Sep 2007 16:08:00 +0200 wenzelm simplified type int (eliminated IntInf.int, integer);
Sat, 15 Sep 2007 19:27:35 +0200 haftmann fixed title
Thu, 16 Aug 2007 21:52:07 +0200 wenzelm removed dead code;
Tue, 31 Jul 2007 00:56:26 +0200 wenzelm arith method setup: proper context;
Fri, 20 Jul 2007 14:28:25 +0200 haftmann moved class ord from Orderings.thy to HOL.thy
Tue, 10 Jul 2007 17:30:54 +0200 haftmann now works with SML/NJ
Tue, 10 Jul 2007 09:23:15 +0200 haftmann replaced code generator framework for reflected cooper
Thu, 05 Jul 2007 00:06:20 +0200 wenzelm avoid polymorphic equality;
less more (0) -60 tip