20051208 
wenzelm 
20051208 
tuned sources and proofs

file  diff  annotate 
20050712 
avigad 
20050712 
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
added lemmas to Ring_and_Field.thy (reasoning about signs, fractions, etc.)
renamed simplification rules for abs (abs_of_pos, etc.)
renamed rules for multiplication and signs (mult_pos_pos, etc.)
moved lemmas involving fractions from NatSimprocs.thy
added setsum_mono3 to FiniteSet.thy
added simplification rules for powers to Parity.thy

file  diff  annotate 
20050707 
nipkow 
20050707 
linear arithmetic now takes "&" in assumptions apart.

file  diff  annotate 
20050701 
nipkow 
20050701 
prime is a predicate now.

file  diff  annotate 
20050617 
haftmann 
20050617 
migrated theory headers to new format

file  diff  annotate 
20041209 
nipkow 
20041209 
First step in reorganizing Finite_Set

file  diff  annotate 
20040621 
kleing 
20040621 
Merged in license change from Isabelle2004

file  diff  annotate 
20040112 
paulson 
20040112 
Added lemmas to Ring_and_Field with slightly modified simplification rules
Deleted some littleused integer theorems, replacing them by the generic ones
in Ring_and_Field
Consolidated integer powers

file  diff  annotate 
20031203 
paulson 
20031203 
Simplification of the development of Integers

file  diff  annotate 
20030320 
paulson 
20030320 
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer

file  diff  annotate 