2002-10-21 berghofe [Mon, 21 Oct 2002 17:07:27 +0200] rev 13659
Removed obsolete functions dealing with flex-flex constraints.
src/Pure/drule.ML src/Pure/logic.ML

2002-10-21 berghofe [Mon, 21 Oct 2002 17:04:47 +0200] rev 13658
Changed handling of flex-flex constraints: now stored in separate
tpairs field of theorem record.
src/Pure/display.ML src/Pure/thm.ML

2002-10-21 berghofe [Mon, 21 Oct 2002 17:00:45 +0200] rev 13657
Now applies standard' to "unfold" theorem (due to flex-flex constraints).
src/HOL/Tools/inductive_package.ML

2002-10-21 berghofe [Mon, 21 Oct 2002 16:57:39 +0200] rev 13656
Changed type of Logic.strip_horn.
src/HOL/Tools/datatype_realizer.ML

2002-10-18 paulson [Fri, 18 Oct 2002 17:50:13 +0200] rev 13655
Tidying up. New primitives is_iterates and is_iterates_fm.
src/ZF/Constructible/DPow_absolute.thy src/ZF/Constructible/Datatype_absolute.thy src/ZF/Constructible/Internalize.thy src/ZF/Constructible/L_axioms.thy src/ZF/Constructible/Rec_Separation.thy src/ZF/Constructible/Satisfies_absolute.thy

2002-10-18 nipkow [Fri, 18 Oct 2002 09:53:18 +0200] rev 13654
Mod due to: Added a few thms about UN/INT/{}/UNIV
src/HOL/Algebra/abstract/Ideal.ML

2002-10-18 nipkow [Fri, 18 Oct 2002 09:53:02 +0200] rev 13653
Added a few thms about UN/INT/{}/UNIV
src/HOL/Set.ML src/HOL/Set.thy

2002-10-17 paulson [Thu, 17 Oct 2002 10:56:00 +0200] rev 13652
fixed comments and types
src/HOL/Library/Zorn.thy

2002-10-17 paulson [Thu, 17 Oct 2002 10:54:11 +0200] rev 13651
Cosmetic changes suggested by writing the paper. Deleted some
redundant arity proofs
src/ZF/Constructible/Formula.thy src/ZF/Constructible/Internalize.thy src/ZF/Constructible/L_axioms.thy src/ZF/Constructible/Rec_Separation.thy

2002-10-17 paulson [Thu, 17 Oct 2002 10:52:59 +0200] rev 13650
fixing the cut_tac method to work when there are no instantiations and the
supplied theorems have premises
src/Pure/Isar/method.ML src/Pure/drule.ML src/Pure/tactic.ML src/Pure/tctical.ML