src/HOL/Word/Bit_Representation.thy
Tue, 13 Dec 2011 19:21:36 +0100 huffman add simp rules for bintrunc applied to numerals
Tue, 13 Dec 2011 13:21:48 +0100 huffman add simp rules for bin_rest and bin_last applied to numerals
Tue, 13 Dec 2011 13:10:25 +0100 huffman add simp rules for bin_sign applied to numerals
Tue, 13 Dec 2011 13:05:44 +0100 huffman add simp rules for BIT applied to numerals
Tue, 13 Dec 2011 12:55:36 +0100 huffman declare BIT_eq_iff [iff]; remove unneeded lemmas
Tue, 13 Dec 2011 12:36:41 +0100 huffman towards removing BIT_simps from the simpset
Tue, 13 Dec 2011 12:10:43 +0100 huffman type signature for bin_sign
Tue, 13 Dec 2011 12:05:47 +0100 huffman remove some unwanted numeral-representation-specific simp rules
Tue, 13 Dec 2011 11:48:59 +0100 huffman remove redundant lemmas
Tue, 13 Dec 2011 11:26:10 +0100 huffman reorder some definitions and proofs, in preparation for new numeral representation
Sun, 20 Nov 2011 20:59:30 +0100 wenzelm eliminated obsolete "standard";
Thu, 17 Nov 2011 12:29:48 +0100 huffman HOL-Word: add simp rules for bin_rest, bin_last; shorten several proofs
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
Fri, 16 Sep 2011 12:10:43 +1000 kleing removed unused legacy lemma names, some comment cleanup.
Mon, 12 Sep 2011 07:55:43 +0200 nipkow new fastforce replacing fastsimp - less confusing name
Wed, 29 Dec 2010 17:34:41 +0100 wenzelm explicit file specifications -- avoid secondary load path;
Thu, 01 Jul 2010 13:32:14 +0200 haftmann avoid bitstrings in generated code
Wed, 30 Jun 2010 16:45:47 +0200 haftmann more speaking names
less more (0) tip