src/HOL/Word/Word.thy
Thu, 23 Feb 2012 15:37:42 +0100 huffman make bool list functions respect int/bin distinction
Thu, 23 Feb 2012 13:16:18 +0100 huffman make uses of bin_sign respect int/bin distinction
Thu, 23 Feb 2012 12:45:00 +0100 huffman removed unnecessary lemma zero_bintrunc
Thu, 23 Feb 2012 12:24:34 +0100 huffman remove unnecessary lemmas
Wed, 08 Feb 2012 01:49:33 +0100 blanchet use 'primrec' to define "rotate1", for uniformity (and to help first-order tools that rely on "Spec_Rules")
Tue, 10 Jan 2012 15:43:16 +0100 huffman add simp rules for set_bit and msb applied to 0 and 1
Tue, 10 Jan 2012 14:48:42 +0100 huffman add simp rule test_bit_1
Fri, 06 Jan 2012 16:42:15 +0100 wenzelm recovered case syntax for of_int, also with source positions (appears to be unused nonetheless);
Thu, 05 Jan 2012 15:31:49 +0100 wenzelm misc tuning;
Fri, 30 Dec 2011 16:08:35 +0100 huffman add simp rules for bitwise word operations with 1
Fri, 30 Dec 2011 11:11:57 +0100 huffman remove unnecessary intermediate lemmas
Thu, 29 Dec 2011 10:47:54 +0100 haftmann semiring_numeral_0_eq_0, semiring_numeral_1_eq_1 now [simp], superseeding corresponding simp rules on type nat
Wed, 28 Dec 2011 22:08:44 +0100 wenzelm merged
Wed, 28 Dec 2011 20:05:28 +0100 huffman restate some lemmas to respect int/bin distinction
Wed, 28 Dec 2011 19:15:28 +0100 huffman simplify some proofs
Wed, 28 Dec 2011 18:50:35 +0100 huffman add lemma word_eq_iff
Wed, 28 Dec 2011 18:33:03 +0100 huffman restate lemma word_1_no in terms of Numeral1
Wed, 28 Dec 2011 12:52:23 +0100 huffman remove some duplicate lemmas
Wed, 28 Dec 2011 10:48:39 +0100 huffman simplify proof
Wed, 28 Dec 2011 10:30:43 +0100 huffman replace 'lemmas' with explicit 'lemma'
Wed, 28 Dec 2011 07:58:17 +0100 huffman add section headings
Tue, 27 Dec 2011 18:26:15 +0100 huffman remove duplicate lemma lists
Wed, 28 Dec 2011 20:03:13 +0100 wenzelm reverted some changes for set->predicate transition, according to "hg log -u berghofe -r Isabelle2007:Isabelle2008";
Tue, 27 Dec 2011 15:37:33 +0100 huffman redefine some binary operations on integers work on abstract numerals instead of Int.Pls and Int.Min
Tue, 27 Dec 2011 13:16:22 +0100 huffman remove some uses of Int.succ and Int.pred
Tue, 27 Dec 2011 12:37:11 +0100 huffman remove redundant syntax declaration
Tue, 27 Dec 2011 11:38:55 +0100 huffman declare word_of_int_{0,1} [simp], for consistency with word_of_int_bin
Fri, 23 Dec 2011 16:37:27 +0100 huffman simplify some proofs
Fri, 23 Dec 2011 15:55:23 +0100 huffman remove redundant lemma word_sub_def
Fri, 23 Dec 2011 11:50:12 +0100 huffman remove two conflicting simp rules for 'number_of (number_of _)' pattern
Wed, 14 Dec 2011 08:32:48 +0100 huffman replace 'lemmas' with 'lemma'
Tue, 13 Dec 2011 12:36:41 +0100 huffman towards removing BIT_simps from the simpset
Mon, 12 Dec 2011 08:19:37 +0100 huffman replace more uses of 'lemmas' with explicit 'lemma';
Sun, 11 Dec 2011 09:55:57 +0100 huffman replace many uses of 'lemmas' with 'lemma';
Sat, 10 Dec 2011 22:00:42 +0100 huffman prove class instances without extra lemmas
Sat, 10 Dec 2011 21:48:16 +0100 huffman finite class instance for word type; remove unused lemmas
Sat, 10 Dec 2011 21:07:59 +0100 huffman remove unused lemmas
Sat, 10 Dec 2011 16:24:22 +0100 huffman generalize some lemmas
Sat, 10 Dec 2011 08:29:19 +0100 huffman tidied Word.thy;
Fri, 09 Dec 2011 14:52:51 +0100 huffman remove redundant lemma word_diff_minus
Wed, 30 Nov 2011 16:27:10 +0100 wenzelm prefer typedef without extra definition and alternative name;
Wed, 23 Nov 2011 22:59:39 +0100 wenzelm modernized some old-style infix operations, which were left over from the time of ML proof scripts;
Sun, 20 Nov 2011 20:59:30 +0100 wenzelm eliminated obsolete "standard";
Fri, 18 Nov 2011 06:50:05 +0100 huffman Word.thy: reduce usage of numeral-representation-dependent thms like number_of_is_id in proofs
Fri, 18 Nov 2011 04:56:35 +0100 huffman merged
Thu, 17 Nov 2011 15:07:46 +0100 huffman HOL-Word: removed more duplicate theorems
Thu, 17 Nov 2011 14:52:05 +0100 huffman HOL-Word: removed many duplicate theorems (see NEWS)
Thu, 17 Nov 2011 14:24:10 +0100 huffman Word.thy: rearrange to instantiate arithmetic classes together with arithmetic operations
Thu, 17 Nov 2011 12:38:03 +0100 huffman move definitions of bitwise operators into appropriate document section
Thu, 17 Nov 2011 21:58:10 +0100 wenzelm eliminated slightly odd Rep' with dynamically-scoped [simplified];
Wed, 16 Nov 2011 13:58:31 +0100 huffman remove redundant lemmas bin_last_mod and bin_rest_div, use bin_last_def and bin_rest_def instead
Wed, 16 Nov 2011 12:29:50 +0100 huffman simplify proof of word_of_int; remove several now-unused lemmas about Rep_Integ
Fri, 28 Oct 2011 11:02:27 +0200 huffman use simproc_setup for cancellation simprocs, to get proper name bindings
Fri, 16 Sep 2011 12:10:15 +1000 kleing removed word_neq_0_conv from simpset, it's almost never wanted.
Mon, 12 Sep 2011 07:55:43 +0200 nipkow new fastforce replacing fastsimp - less confusing name
Wed, 07 Sep 2011 09:02:58 -0700 huffman avoid using legacy theorem names
Wed, 07 Sep 2011 00:08:09 +0200 wenzelm tuned proofs;
Fri, 13 May 2011 22:55:00 +0200 wenzelm proper Proof.context for classical tactics;
Fri, 14 Jan 2011 15:44:47 +0100 wenzelm eliminated global prems;
Wed, 29 Dec 2010 17:34:41 +0100 wenzelm explicit file specifications -- avoid secondary load path;
less more (0) -60 tip