20101229 
wenzelm 
20101229 
explicit file specifications  avoid secondary load path;

file  diff  annotate 
20100321 
wenzelm 
20100321 
standard headers;

file  diff  annotate 
20100321 
wenzelm 
20100321 
slightly more uniform definitions  eliminated oldstyle metaequality;

file  diff  annotate 
20091015 
wenzelm 
20091015 
tuned proof (via atp_minimized);

file  diff  annotate 
20090901 
haftmann 
20090901 
some reorganization of number theory

file  diff  annotate 
20090707 
nipkow 
20090707 
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int

file  diff  annotate 
20090618 
huffman 
20090618 
fix name clash with old/new prime libraries

file  diff  annotate 
20090304 
blanchet 
20090304 
Merge.

file  diff  annotate 
20090304 
blanchet 
20090304 
Merge.

file  diff  annotate 
20090221 
nipkow 
20090221 
Removed subsumed lemmas

file  diff  annotate 
20090220 
haftmann 
20090220 
consider changes variable names in theorem le_imp_power_dvd

file  diff  annotate 
20080801 
ballarin 
20080801 
Generalised polynomial lemmas from cring to ring.

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 
20071023 
nipkow 
20071023 
went back to >0

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 
20070927 
paulson 
20070927 
removal of some "ref"s from res_axioms.ML; a sideeffect is that the ordering
theorems of Nat.thy are hidden by the Ordering.thy versions

file  diff  annotate 
20070724 
wenzelm 
20070724 
fixed proofs involving dvd;

file  diff  annotate 
20061108 
wenzelm 
20061108 
moved theories Parity, GCD, Binomial to Library;

file  diff  annotate 
20060830 
webertj 
20060830 
lin_arith_prover: splitting reverted because of performance loss

file  diff  annotate 
20060803 
ballarin 
20060803 
Restructured algebra library, added ideals and quotient rings.

file  diff  annotate 
20060802 
webertj 
20060802 
lin_arith_prover splits certain operators (e.g. min, max, abs)

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 
20040609 
paulson 
20040609 
moved some cardinality results into main HOL

file  diff  annotate 
20040506 
wenzelm 
20040506 
tuned document;

file  diff  annotate 
20030318 
paulson 
20030318 
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
to the new Group setup.
Deleted Ring, Module from GroupTheory
Minor UNITY changes

file  diff  annotate 