2008-06-10 wenzelm [Tue, 10 Jun 2008 16:43:16 +0200] rev 27118
tuned proofs;
src/HOL/MicroJava/J/JTypeSafe.thy

2008-06-10 wenzelm [Tue, 10 Jun 2008 16:43:14 +0200] rev 27117
case_split_tac (works without context);
src/HOL/MicroJava/Comp/Index.thy src/HOL/Nominal/Examples/Class.thy src/HOL/TLA/Memory/MemoryImplementation.thy

2008-06-10 wenzelm [Tue, 10 Jun 2008 16:43:07 +0200] rev 27116
tuned;
doc-src/IsarRef/Thy/Proof.thy

2008-06-10 wenzelm [Tue, 10 Jun 2008 16:43:01 +0200] rev 27115
eliminated obsolete case_split_thm -- use case_split;
doc-src/IsarOverview/Isar/Induction.thy src/FOL/FOL.thy src/HOL/Tools/function_package/fundef_core.ML src/HOL/Tools/sat_funcs.ML

2008-06-10 wenzelm [Tue, 10 Jun 2008 16:42:38 +0200] rev 27114
Unstructured induction and cases analysis for Isabelle/HOL.
src/HOL/Tools/induct_tacs.ML

2008-06-10 haftmann [Tue, 10 Jun 2008 15:31:05 +0200] rev 27113
dropped instance with attached definitions
src/Pure/Isar/instance.ML src/Pure/Isar/isar_syn.ML

2008-06-10 haftmann [Tue, 10 Jun 2008 15:31:04 +0200] rev 27112
polished interface of datatype package
src/HOL/Nominal/nominal_atoms.ML src/HOL/Nominal/nominal_package.ML src/HOL/Tools/inductive_realizer.ML src/HOLCF/Tools/domain/domain_theorems.ML

2008-06-10 haftmann [Tue, 10 Jun 2008 15:31:03 +0200] rev 27111
adjusted some proofs involving inats
src/HOLCF/FOCUS/Fstreams.thy src/HOLCF/ex/Stream.thy

2008-06-10 haftmann [Tue, 10 Jun 2008 15:31:02 +0200] rev 27110
refactoring; addition, numerals
src/HOL/Library/Nat_Infinity.thy

2008-06-10 haftmann [Tue, 10 Jun 2008 15:31:01 +0200] rev 27109
more instantiation
src/HOL/Library/ListVector.thy