20090128 
nipkow 
20090128 
merged  resolving conflics

file  diff  annotate 
20090128 
nipkow 
20090128 
Replaced group_ and ring_simps by algebra_simps;
removed compare_rls  use algebra_simps now

file  diff  annotate 
20090126 
haftmann 
20090126 
stripped Id

file  diff  annotate 
20080919 
huffman 
20080919 
avoid using implicit assumptions

file  diff  annotate 
20080829 
haftmann 
20080829 
fixed names of class assumptions

file  diff  annotate 
20080721 
haftmann 
20080721 
(re)added simp rules for (_ + _) div/mod _

file  diff  annotate 
20080718 
haftmann 
20080718 
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas

file  diff  annotate 
20080610 
haftmann 
20080610 
slightly tuning of some proofs involving case distinction and induction on natural numbers and similar

file  diff  annotate 
20080409 
huffman 
20080409 
move lemmas from Word/BinBoolList.thy to List.thy

file  diff  annotate 
20080404 
haftmann 
20080404 
more new primrec

file  diff  annotate 
20080217 
huffman 
20080217 
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1

file  diff  annotate 
20080128 
wenzelm 
20080128 
eliminated escaped white space;

file  diff  annotate 
20080115 
haftmann 
20080115 
joined theories IntDef, Numeral, IntArith to theory Int

file  diff  annotate 
20071108 
wenzelm 
20071108 
eliminated illegal schematic variables in where/of;

file  diff  annotate 
20071021 
nipkow 
20071021 
Eliminated most of the neq0_conv occurrences. As a result, many
theorems had to be rephrased with ~= 0 instead of > 0.

file  diff  annotate 
20071020 
chaieb 
20071020 
fixed proofs

file  diff  annotate 
20070828 
huffman 
20070828 
revert to Word library version from 2007/08/20

file  diff  annotate 
20070822 
huffman 
20070822 
move if_simps from BinBoolList to Num_Lemmas

file  diff  annotate 
20070822 
huffman 
20070822 
move bool list stuff from BinOperations to BinBoolList;
reorganize BinBoolList into subsections

file  diff  annotate 
20070820 
huffman 
20070820 
use overloaded bitwise operators at type int

file  diff  annotate 
20070820 
huffman 
20070820 
headers for document generation

file  diff  annotate 
20070820 
kleing 
20070820 
* HOLWord:
New extensive library and type for generic, fixed size machine
words, with arithemtic, bitwise, shifting and rotating operations,
reflection into int, nat, and bool lists, automation for linear
arithmetic (by automatic reflection into nat or int), including
lemmas on overflow and monotonicity. Instantiated to all appropriate
arithmetic type classes, supporting automatic simplification of
numerals on all operations. Jointly developed by NICTA, Galois, and
PSU.
* still to do: README.html/document + moving some of the generic lemmas
to appropriate place in distribution

file  diff  annotate 