2007-08-07 haftmann [Tue, 07 Aug 2007 09:38:48 +0200] rev 24165
more robust simproces
src/HOL/Bali/Eval.thy src/HOL/Bali/Evaln.thy

2007-08-07 haftmann [Tue, 07 Aug 2007 09:38:47 +0200] rev 24164
tuned
src/HOL/Lattices.thy

2007-08-07 haftmann [Tue, 07 Aug 2007 09:38:46 +0200] rev 24163
simplified proofs
src/HOL/Finite_Set.thy

2007-08-07 haftmann [Tue, 07 Aug 2007 09:38:44 +0200] rev 24162
split off theory Option for benefit of code generator
src/HOL/Bali/Basis.thy src/HOL/Datatype.thy src/HOL/Extraction.thy src/HOL/FunDef.thy src/HOL/IsaMakefile src/HOL/Nat.thy src/HOL/Nominal/nominal_atoms.ML src/HOL/Product_Type.thy

2007-08-07 haftmann [Tue, 07 Aug 2007 09:38:43 +0200] rev 24161
changed import order
src/HOL/ATP_Linkup.thy

2007-08-06 wenzelm [Mon, 06 Aug 2007 19:59:07 +0200] rev 24160
added more instances;
src/Pure/ML-Systems/overloading_smlnj.ML

2007-08-06 wenzelm [Mon, 06 Aug 2007 19:58:59 +0200] rev 24159
ML-Systems/overloading_smlnj.ML;
src/Pure/IsaMakefile

2007-08-06 wenzelm [Mon, 06 Aug 2007 19:35:43 +0200] rev 24158
Overloading in SML/NJ.
src/Pure/ML-Systems/overloading_smlnj.ML

2007-08-06 berghofe [Mon, 06 Aug 2007 16:08:01 +0200] rev 24157
Added renaming function to prevent correctness proof for realizer
of induction rule to fail because of name clashes between parameters
and predicate variables.
src/HOL/Tools/inductive_realizer.ML

2007-08-06 berghofe [Mon, 06 Aug 2007 16:05:25 +0200] rev 24156
No document for Pretty_Int theory.
src/HOL/Lambda/ROOT.ML