src/HOL/Library/Word.thy
Sat, 19 Dec 2020 17:49:14 +0000 haftmann more precise simpset for method unat_arith
Sat, 05 Dec 2020 19:24:36 +0000 haftmann moved some lemmas from AFP to distribution
Thu, 26 Nov 2020 18:09:02 +0000 paulson Stepan Holub's stronger version of comm_append_are_replicate, and a de-applied Word.thy
Sun, 15 Nov 2020 10:13:03 +0000 haftmann official collection for bit projection simplifications
Thu, 29 Oct 2020 10:03:03 +0000 haftmann moved most material from session HOL-Word to Word_Lib in the AFP
Tue, 02 Mar 2010 12:26:50 +0100 krauss killed more recdefs
Wed, 17 Feb 2010 10:30:36 -0800 huffman fix more looping simp rules
Thu, 21 Jan 2010 09:27:57 +0100 haftmann merged
Sat, 16 Jan 2010 17:15:28 +0100 haftmann dropped some old primrecs and some constdefs
Sun, 10 Jan 2010 18:43:45 +0100 berghofe Adapted to changes in induct method.
Fri, 30 Oct 2009 13:59:50 +0100 haftmann tuned proof
Sat, 17 Oct 2009 14:43:18 +0200 wenzelm eliminated hard tabulators, guessing at each author's individual tab-width;
Mon, 31 Aug 2009 14:09:42 +0200 nipkow tuned the simp rules for Int involving insert and intervals.
Fri, 28 Aug 2009 19:35:49 +0200 nipkow tuned proofs
Wed, 22 Apr 2009 19:09:21 +0200 haftmann power operation defined generic
Tue, 03 Mar 2009 17:05:18 +0100 nipkow removed and renamed redundant lemmas
Fri, 10 Oct 2008 06:45:53 +0200 haftmann `code func` now just `code`
Tue, 16 Sep 2008 09:21:26 +0200 haftmann dropped superfluous code lemmas
Mon, 07 Jul 2008 08:47:17 +0200 haftmann absolute imports of HOL/*.thy theories
Thu, 26 Jun 2008 10:07:01 +0200 haftmann established Plain theory and image
Tue, 10 Jun 2008 15:30:56 +0200 haftmann removed some dubious code lemmas
Sat, 29 Mar 2008 22:55:49 +0100 wenzelm purely functional setup of claset/simpset/clasimpset;
Sun, 17 Feb 2008 06:49:53 +0100 huffman New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
Fri, 25 Jan 2008 14:53:52 +0100 haftmann moved definition of power on ints to theory Int
Tue, 15 Jan 2008 16:19:23 +0100 haftmann joined theories IntDef, Numeral, IntArith to theory Int
Mon, 10 Dec 2007 11:24:12 +0100 haftmann switched import from Main to List
Tue, 23 Oct 2007 23:27:23 +0200 nipkow went back to >0
Sun, 21 Oct 2007 14:53:44 +0200 nipkow Eliminated most of the neq0_conv occurrences. As a result, many
Sat, 20 Oct 2007 12:09:33 +0200 chaieb fixed proofs
Tue, 17 Jul 2007 14:38:00 +0200 krauss reverted fun->recdef, since there are problems with induction rule
Mon, 16 Jul 2007 21:39:56 +0200 krauss use function package
Sat, 23 Jun 2007 19:33:22 +0200 nipkow tuned and renamed group_eq_simps and ring_eq_simps
Wed, 20 Jun 2007 05:18:39 +0200 huffman change simp rules for of_nat to work like int did previously (reorient of_nat_Suc, remove of_nat_mult [simp]); preserve original variable names in legacy int theorems
Wed, 13 Jun 2007 18:30:16 +0200 wenzelm tuned proofs: avoid implicit prems;
Wed, 13 Jun 2007 03:31:11 +0200 huffman removed constant int :: nat => int;
Thu, 17 May 2007 19:49:16 +0200 haftmann tuned
Thu, 11 Jan 2007 16:53:12 +0100 paulson well-founded relations for the integers
Fri, 17 Nov 2006 02:20:03 +0100 wenzelm more robust syntax for definition/abbreviation/notation;
Tue, 07 Nov 2006 11:47:57 +0100 wenzelm renamed 'const_syntax' to 'notation';
Wed, 06 Sep 2006 13:48:02 +0200 haftmann got rid of Numeral.bin type
Wed, 26 Jul 2006 19:23:04 +0200 webertj linear arithmetic splits certain operators (e.g. min, max, abs)
Sat, 27 May 2006 17:42:02 +0200 wenzelm tuned;
Mon, 26 Sep 2005 15:17:33 +0200 skalberg Made sure all lemmas now have names (especially so that certain of them
Wed, 13 Jul 2005 15:06:20 +0200 paulson generlization of some "nat" theorems
Fri, 17 Jun 2005 16:12:49 +0200 haftmann migrated theory headers to new format
Wed, 23 Mar 2005 12:09:18 +0100 paulson replaced bool by a new datatype "bit" for binary numerals
Wed, 02 Feb 2005 18:06:25 +0100 paulson tidying of some subst/simplesubst proofs
Tue, 01 Feb 2005 18:01:57 +0100 paulson the new subst tactic, by Lucas Dixon
Wed, 24 Nov 2004 10:32:33 +0100 berghofe Functions nat_to_bv and bv_to_nat now really operate on natural numbers.
Wed, 18 Aug 2004 11:09:40 +0200 nipkow import -> imports
Mon, 16 Aug 2004 14:22:27 +0200 nipkow New theory header syntax.
Tue, 20 Jul 2004 14:23:09 +0200 paulson removed some obsolete proofs
Thu, 01 Jul 2004 12:29:53 +0200 paulson new treatment of binary numerals
Thu, 06 May 2004 14:14:18 +0200 wenzelm tuned document;
Fri, 16 Apr 2004 13:51:04 +0200 wenzelm tuned document;
Wed, 14 Apr 2004 14:13:05 +0200 kleing use more symbols in HTML output
Mon, 29 Mar 2004 15:35:04 +0200 skalberg Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
less more (0) tip