2004-01-08 kleing [Thu, 08 Jan 2004 08:14:00 +0100] rev 14345
separate thm lists in latex output by \isasep
lib/texinputs/isabelle.sty src/Pure/Isar/isar_output.ML

2004-01-08 kleing [Thu, 08 Jan 2004 04:32:52 +0100] rev 14344
run makeindex if necessary
etc/settings lib/Tools/document lib/Tools/latex

2004-01-07 kleing [Wed, 07 Jan 2004 07:52:12 +0100] rev 14343
map_idI
src/HOL/List.thy

2004-01-06 paulson [Tue, 06 Jan 2004 10:50:36 +0100] rev 14342
auto update
doc-src/TutorialI/isabelle.sty

2004-01-06 paulson [Tue, 06 Jan 2004 10:40:15 +0100] rev 14341
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
This allows more theorems to be proved for semirings, but
requires a redundant axiom to be proved for rings, etc.
src/HOL/Complex/Complex.thy src/HOL/Complex/NSComplex.thy src/HOL/Hyperreal/HyperDef.thy src/HOL/Integ/Int.thy src/HOL/Integ/IntDef.thy src/HOL/Library/Rational_Numbers.thy src/HOL/Nat.thy src/HOL/Real/Complex_Numbers.thy src/HOL/Real/RealDef.thy src/HOL/Ring_and_Field.thy

2004-01-06 paulson [Tue, 06 Jan 2004 10:38:14 +0100] rev 14340
correction to cterm_instantiate by Christoph Leuth
src/Pure/drule.ML

2004-01-05 nipkow [Mon, 05 Jan 2004 23:10:32 +0100] rev 14339
*** empty log message ***
src/HOL/List.thy

2004-01-05 nipkow [Mon, 05 Jan 2004 22:43:03 +0100] rev 14338
*** empty log message ***
src/HOL/List.thy

2004-01-05 nipkow [Mon, 05 Jan 2004 00:46:06 +0100] rev 14337
undid split_comp_eq[simp] because it leads to nontermination together with split_def!
src/HOL/Product_Type.thy src/HOL/Transitive_Closure.thy

2004-01-03 paulson [Sat, 03 Jan 2004 16:09:39 +0100] rev 14336
Deleting more redundant theorems
src/HOL/Complex/ComplexArith0.ML src/HOL/Complex/NSComplex.thy src/HOL/Hyperreal/HRealAbs.ML src/HOL/Hyperreal/HyperPow.ML src/HOL/Hyperreal/Integration.ML src/HOL/Hyperreal/NSA.ML src/HOL/Hyperreal/Transcendental.ML src/HOL/Real/real_arith.ML