wenzelm [Fri, 30 Mar 2012 17:25:34 +0200] rev 48102
merged
wenzelm [Fri, 30 Mar 2012 17:22:17 +0200] rev 48101
tuned proofs, less guesswork;
huffman [Fri, 30 Mar 2012 17:21:36 +0200] rev 48100
merged
huffman [Fri, 30 Mar 2012 16:44:23 +0200] rev 48099
load Tools/numeral.ML in Num.thy
huffman [Fri, 30 Mar 2012 16:43:07 +0200] rev 48098
tuned proof
huffman [Fri, 30 Mar 2012 15:56:12 +0200] rev 48097
set up numeral reorient simproc in Num.thy
huffman [Fri, 30 Mar 2012 15:43:30 +0200] rev 48096
remove redundant simp rule
huffman [Fri, 30 Mar 2012 15:24:24 +0200] rev 48095
add simp rules for eve/odd on numerals
huffman [Fri, 30 Mar 2012 14:27:29 +0200] rev 48094
remove content-free theory ex/Arithmetic_Series_Complex.thy
huffman [Fri, 30 Mar 2012 14:25:32 +0200] rev 48093
rephrase lemmas about arithmetic series using numeral '2'