2009-02-19 huffman [Thu, 19 Feb 2009 17:11:12 -0800] rev 29998
nicer induction/cases rules for numeral types
src/HOL/Library/Numeral_Type.thy

2009-02-19 huffman [Thu, 19 Feb 2009 16:51:46 -0800] rev 29997
number_ring instances for numeral types
src/HOL/Library/Numeral_Type.thy

2009-02-19 huffman [Thu, 19 Feb 2009 12:37:03 -0800] rev 29996
declare xor_compl_{left,right} [simp]
src/HOL/Library/Boolean_Algebra.thy

2009-02-19 huffman [Thu, 19 Feb 2009 12:26:32 -0800] rev 29995
add rule for minus 1 at type bit
src/HOL/Library/Bit.thy

2009-02-19 huffman [Thu, 19 Feb 2009 12:03:31 -0800] rev 29994
add formalization of a type of integers mod 2 to Library
src/HOL/IsaMakefile src/HOL/Library/Bit.thy src/HOL/Library/Library.thy

2009-02-19 huffman [Thu, 19 Feb 2009 09:42:23 -0800] rev 29993
new theory of real inner product spaces
src/HOL/IsaMakefile src/HOL/Library/Inner_Product.thy src/HOL/Library/Library.thy

2009-02-19 huffman [Thu, 19 Feb 2009 09:39:49 -0800] rev 29992
add Powerdomain_ex.thy
src/HOLCF/IsaMakefile src/HOLCF/ex/Powerdomain_ex.thy src/HOLCF/ex/ROOT.ML

2009-02-19 huffman [Thu, 19 Feb 2009 08:07:52 -0800] rev 29991
add more ordering lemmas
src/HOL/ex/Numeral.thy

2009-02-19 huffman [Thu, 19 Feb 2009 06:47:06 -0800] rev 29990
avoid using ab_semigroup_idem_mult locale for powerdomains
src/HOLCF/ConvexPD.thy src/HOLCF/LowerPD.thy src/HOLCF/UpperPD.thy

2009-02-19 huffman [Thu, 19 Feb 2009 05:50:26 -0800] rev 29989
merged