2008-01-02 haftmann [Wed, 02 Jan 2008 15:14:02 +0100] rev 25762
splitted class uminus from class minus
src/HOL/Algebra/abstract/Ring2.thy src/HOL/Algebra/poly/PolyHomo.thy src/HOL/Algebra/poly/UnivPoly2.thy src/HOL/HOL.thy src/HOL/Hyperreal/StarDef.thy src/HOL/Import/HOL/realax.imp src/HOL/IntDef.thy src/HOL/OrderedGroup.thy src/HOL/Real/HahnBanach/FunctionOrder.thy src/HOL/Real/HahnBanach/Linearform.thy src/HOL/Real/HahnBanach/NormedSpace.thy src/HOL/Real/HahnBanach/Subspace.thy src/HOL/Real/Rational.thy src/HOL/Real/RealDef.thy src/HOL/Ring_and_Field.thy src/HOL/Set.thy src/HOL/Tools/Qelim/cooper_data.ML src/HOL/Word/BinOperations.thy src/HOL/Word/BitSyntax.thy src/HOL/Word/WordArith.thy src/HOL/Word/WordDefinition.thy

2008-01-02 paulson [Wed, 02 Jan 2008 12:22:38 +0100] rev 25761
testing for empty sort
src/HOL/Tools/metis_tools.ML src/HOL/Tools/res_atp.ML src/HOL/Tools/res_axioms.ML

2008-01-02 paulson [Wed, 02 Jan 2008 12:22:05 +0100] rev 25760
new metis proofs
src/HOL/NumberTheory/Euler.thy

2008-01-02 kleing [Wed, 02 Jan 2008 04:10:47 +0100] rev 25759
renamed foldM to fold_mset on general request
added Tobias' lemmas on fold_mset (A+B) etc
tuned default simp set for fold_mset
src/HOL/Library/Multiset.thy

2008-01-02 huffman [Wed, 02 Jan 2008 01:20:18 +0100] rev 25758
update instance proofs to new style
src/HOLCF/Ffun.thy

2008-01-01 huffman [Tue, 01 Jan 2008 20:35:16 +0100] rev 25757
declare sprodE as cases rule; new induction rule sprod_induct
src/HOLCF/Sprod.thy

2008-01-01 huffman [Tue, 01 Jan 2008 20:30:16 +0100] rev 25756
add induction rule ssum_induct
src/HOLCF/Ssum.thy

2008-01-01 wenzelm [Tue, 01 Jan 2008 16:09:29 +0100] rev 25755
eval_wrapper: CRITICAL;
tuned;
src/Pure/ML/ml_context.ML

2008-01-01 wenzelm [Tue, 01 Jan 2008 16:09:28 +0100] rev 25754
try_ml_file: setmp explicit theory context, prevents race condition wrt. concurrent ML_Context.set_context;
src/Pure/Isar/outer_syntax.ML

2008-01-01 wenzelm [Tue, 01 Jan 2008 16:09:27 +0100] rev 25753
tuned spaces;
src/Pure/General/secure.ML