2008-04-07 haftmann [Mon, 07 Apr 2008 15:37:34 +0200] rev 26567
instantiation replacing primitive instance plus overloaded defs; more conservative type arities
src/HOL/Library/Multiset.thy

2008-04-07 haftmann [Mon, 07 Apr 2008 15:37:33 +0200] rev 26566
instantiation replacing primitive instance plus overloaded defs
src/HOL/Bali/Decl.thy src/HOL/Hyperreal/HyperDef.thy

2008-04-07 haftmann [Mon, 07 Apr 2008 15:37:32 +0200] rev 26565
instantiation replacing primitive instance plus overloaded defs; realpow.simps now named power_real.simps
src/HOL/Real/RealPow.thy

2008-04-07 haftmann [Mon, 07 Apr 2008 15:37:31 +0200] rev 26564
explicit definition for "/"
src/HOL/Real/PReal.thy

2008-04-07 haftmann [Mon, 07 Apr 2008 15:37:30 +0200] rev 26563
explicit dummy instantiation for div
src/HOL/Algebra/poly/UnivPoly2.thy

2008-04-07 paulson [Mon, 07 Apr 2008 15:37:27 +0200] rev 26562
* Metis: the maximum number of clauses that can be produced from a theorem is now given by the attribute max_clauses. Theorems that exceed this number are ignored, with a warning printed.
NEWS src/HOL/Hilbert_Choice.thy src/HOL/Tools/meson.ML src/HOL/Tools/res_axioms.ML

2008-04-07 paulson [Mon, 07 Apr 2008 15:37:04 +0200] rev 26561
Superficial changes
CVS: ----------------------------------------------------------------------
src/HOL/Tools/metis_tools.ML

2008-04-04 haftmann [Fri, 04 Apr 2008 13:40:27 +0200] rev 26560
tuned
src/HOL/Word/Num_Lemmas.thy src/HOL/Word/Size.thy src/HOL/Word/TdThs.thy src/HOL/Word/WordArith.thy src/HOL/Word/WordMain.thy

2008-04-04 haftmann [Fri, 04 Apr 2008 13:40:26 +0200] rev 26559
syntactic classes for bit operations
src/HOL/Word/BitSyntax.thy src/HOL/Word/WordDefinition.thy

2008-04-04 haftmann [Fri, 04 Apr 2008 13:40:25 +0200] rev 26558
renamed app2 to map2
src/HOL/Word/BinOperations.thy src/HOL/Word/WordBitwise.thy src/HOL/Word/WordGenLib.thy src/HOL/Word/WordShift.thy