2002-07-28 wenzelm [Sun, 28 Jul 2002 21:09:37 +0200] rev 13427
tuned document;
src/ZF/Constructible/document/root.tex src/ZF/IsaMakefile

2002-07-27 wenzelm [Sat, 27 Jul 2002 21:55:14 +0200] rev 13426
make SML/NJ happy;
src/Pure/Isar/proof_context.ML

2002-07-26 wenzelm [Fri, 26 Jul 2002 21:09:39 +0200] rev 13425
support for split assumptions in cases (hyps vs. prems);
NEWS doc-src/IsarRef/generic.tex src/Provers/induct_method.ML src/Pure/Isar/proof.ML src/Pure/Isar/proof_context.ML src/Pure/Isar/rule_cases.ML

2002-07-26 wenzelm [Fri, 26 Jul 2002 21:07:57 +0200] rev 13424
tuned;
src/Pure/pure_thy.ML

2002-07-25 paulson [Thu, 25 Jul 2002 18:29:04 +0200] rev 13423
More lemmas, working towards relativization of "satisfies"
src/ZF/Constructible/Datatype_absolute.thy src/ZF/Constructible/Relative.thy

2002-07-25 paulson [Thu, 25 Jul 2002 10:56:35 +0200] rev 13422
Added the assumption nth_replacement to locale M_datatypes.
Moved up its proof to make it available for the instantiation of that locale.
src/ZF/Constructible/Datatype_absolute.thy src/ZF/Constructible/Rec_Separation.thy

2002-07-24 wenzelm [Wed, 24 Jul 2002 22:15:55 +0200] rev 13421
simplified locale predicates;
src/HOL/Finite_Set.thy src/HOL/HOL.thy src/HOL/NumberTheory/IntFact.thy src/HOL/Record.thy src/HOL/Set.thy src/HOL/Typedef.thy src/HOL/Unix/Unix.thy src/ZF/AC/AC18_AC19.thy

2002-07-24 wenzelm [Wed, 24 Jul 2002 22:14:42 +0200] rev 13420
removed unused locale_facts(_i);
simplified locale predicates: only one level for zero imports;
tuned;
src/Pure/Isar/locale.ML

2002-07-24 wenzelm [Wed, 24 Jul 2002 22:13:02 +0200] rev 13419
tuned;
src/HOL/Tools/record_package.ML src/HOL/ex/Locales.thy

2002-07-24 paulson [Wed, 24 Jul 2002 17:59:12 +0200] rev 13418
tweaks, aiming towards relativization of "satisfies"
src/ZF/Constructible/Datatype_absolute.thy src/ZF/Constructible/L_axioms.thy src/ZF/Constructible/Rec_Separation.thy src/ZF/Constructible/Relative.thy src/ZF/Constructible/WF_absolute.thy