src/HOL/Decision_Procs/MIR.thy
Thu, 03 Mar 2011 15:19:20 +0100 wenzelm removed spurious 'unused_thms' (cf. 1a65b780bd56);
Fri, 25 Feb 2011 20:07:48 +0100 nipkow Some cleaning up
Thu, 24 Feb 2011 21:54:28 +0100 krauss recdef -> fun(ction)
Thu, 24 Feb 2011 17:38:05 +0100 krauss eliminated clones of List.upto
Mon, 21 Feb 2011 23:47:19 +0100 wenzelm tuned proofs -- eliminated prems;
Fri, 07 Jan 2011 18:10:42 +0100 bulwahn adopting proofs due to new list comprehension to set comprehension simproc
Wed, 29 Dec 2010 17:34:41 +0100 wenzelm explicit file specifications -- avoid secondary load path;
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
Mon, 19 Jul 2010 16:09:44 +0200 haftmann diff_minus subsumes diff_def
Wed, 12 May 2010 12:31:51 +0200 haftmann tuned test problems
Sun, 09 May 2010 22:51:11 -0700 huffman avoid using real-specific versions of generic lemmas
Thu, 29 Apr 2010 15:00:40 +0200 haftmann code_reflect: specify module name directly after keyword
Wed, 28 Apr 2010 21:41:05 +0200 haftmann use code_reflect
Mon, 01 Mar 2010 13:40:23 +0100 haftmann replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
Fri, 05 Feb 2010 14:33:50 +0100 haftmann more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
Thu, 12 Nov 2009 17:21:48 +0100 hoelzl New list theorems; added map_map to simpset, this is the prefered direction; allow sorting by a key
Thu, 22 Oct 2009 13:48:06 +0200 haftmann map_range (and map_index) combinator
Sat, 17 Oct 2009 14:43:18 +0200 wenzelm eliminated hard tabulators, guessing at each author's individual tab-width;
Tue, 07 Jul 2009 17:39:51 +0200 nipkow renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
Sat, 20 Jun 2009 13:34:54 +0200 nipkow added lemmas; tuned
Wed, 17 Jun 2009 16:55:01 -0700 huffman new GCD library, courtesy of Jeremy Avigad
Sun, 22 Mar 2009 19:36:04 +0100 nipkow 1. New cancellation simprocs for common factors in inequations
Wed, 11 Mar 2009 10:58:18 +0100 hoelzl Updated paths in Decision_Procs comments and NEWS
Wed, 04 Mar 2009 11:05:29 +0100 blanchet Merge.
Wed, 04 Mar 2009 10:45:52 +0100 blanchet Merge.
Thu, 26 Feb 2009 06:33:48 -0800 huffman add type annotation
Wed, 25 Feb 2009 11:29:59 -0800 huffman generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
Sat, 21 Feb 2009 20:52:30 +0100 nipkow Removed subsumed lemmas
Fri, 06 Feb 2009 15:15:32 +0100 haftmann session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
less more (0) tip