2001-12-18 wenzelm [Tue, 18 Dec 2001 16:14:50 +0100] rev 12538
* system: tested support for MacOS X;
NEWS

2001-12-18 paulson [Tue, 18 Dec 2001 15:04:19 +0100] rev 12537
better simplification makes steps redundant
src/ZF/UNITY/UNITY.ML

2001-12-18 paulson [Tue, 18 Dec 2001 15:03:27 +0100] rev 12536
replaced lepoll_lesspoll_lesspoll, lesspoll_lepoll_lesspoll
by lesspoll_trans1, lesspoll_trans2
src/ZF/AC/AC16_WO4.ML src/ZF/AC/AC_Equiv.thy src/ZF/AC/Cardinal_aux.ML src/ZF/AC/DC.ML src/ZF/AC/WO2_AC16.ML src/ZF/Cardinal.ML

2001-12-18 wenzelm [Tue, 18 Dec 2001 14:27:57 +0100] rev 12535
tuned;
doc-src/TutorialI/Rules/rules.tex doc-src/TutorialI/Sets/sets.tex

2001-12-18 wenzelm [Tue, 18 Dec 2001 14:20:38 +0100] rev 12534
use Locale.read/cert_context_statement;
src/Pure/Isar/proof.ML

2001-12-18 nipkow [Tue, 18 Dec 2001 13:15:21 +0100] rev 12533
*** empty log message ***
doc-src/TutorialI/Misc/document/simp.tex doc-src/TutorialI/Misc/simp.thy

2001-12-18 wenzelm [Tue, 18 Dec 2001 02:22:27 +0100] rev 12532
tuned;
src/Pure/Isar/locale.ML

2001-12-18 wenzelm [Tue, 18 Dec 2001 02:20:23 +0100] rev 12531
improved mixfix_args;
src/Pure/Syntax/mixfix.ML

2001-12-18 wenzelm [Tue, 18 Dec 2001 02:20:02 +0100] rev 12530
tuned Type.unify;
do *not* declare TVar names as used;
src/Pure/Isar/proof_context.ML

2001-12-18 wenzelm [Tue, 18 Dec 2001 02:19:31 +0100] rev 12529
simultaneous type-inference of complete context/statement specifications;
reorganized code;
src/Pure/Isar/locale.ML