2007-05-17 huffman [Thu, 17 May 2007 08:42:51 +0200] rev 22987
instance division_ring < no_zero_divisors; clean up field instance proofs
src/HOL/Ring_and_Field.thy

2007-05-17 huffman [Thu, 17 May 2007 08:41:23 +0200] rev 22986
remove redundant instance declaration
src/HOL/OrderedGroup.thy

2007-05-17 huffman [Thu, 17 May 2007 00:45:27 +0200] rev 22985
cleaned up proof of Maclaurin_sin_bound
src/HOL/Hyperreal/MacLaurin.thy

2007-05-16 huffman [Wed, 16 May 2007 23:07:08 +0200] rev 22984
section labels
src/HOL/Hyperreal/Deriv.thy

2007-05-16 huffman [Wed, 16 May 2007 23:03:45 +0200] rev 22983
minimize imports
src/HOL/Complex/Complex_Main.thy src/HOL/Hyperreal/HTranscendental.thy src/HOL/Hyperreal/Hyperreal.thy src/HOL/Hyperreal/MacLaurin.thy src/HOL/Hyperreal/Poly.thy

2007-05-16 chaieb [Wed, 16 May 2007 09:45:22 +0200] rev 22982
dropped |R
src/HOL/Library/Executable_Real.thy

2007-05-15 chaieb [Tue, 15 May 2007 18:28:02 +0200] rev 22981
A verified theory for rational numbers representation and simple calculations;
verified with respect to the real numbers;
src/HOL/IsaMakefile src/HOL/Library/Executable_Real.thy src/HOL/Library/Library.thy src/HOL/ex/ExecutableContent.thy

2007-05-15 berghofe [Tue, 15 May 2007 18:20:07 +0200] rev 22980
Fixed bug that caused proof of induction theorem to fail if
introduction rules contained True or False.
src/HOL/Tools/inductive_package.ML

2007-05-15 huffman [Tue, 15 May 2007 08:10:31 +0200] rev 22979
minimize imports
src/HOL/Complex/CLim.thy

2007-05-15 huffman [Tue, 15 May 2007 07:28:08 +0200] rev 22978
clean up polar_Ex proofs; remove unnecessary lemmas
src/HOL/Hyperreal/Transcendental.thy