2004-08-02 ballarin [Mon, 02 Aug 2004 09:44:46 +0200] rev 15095
Theories now take advantage of recent syntax improvements with (structure).
src/HOL/Algebra/CRing.thy src/HOL/Algebra/FiniteProduct.thy src/HOL/Algebra/Module.thy src/HOL/Algebra/UnivPoly.thy

2004-07-31 paulson [Sat, 31 Jul 2004 20:54:23 +0200] rev 15094
conversion of Hyperreal/{Fact,Filter} to Isar scripts
src/HOL/Hyperreal/Fact.thy src/HOL/Hyperreal/Filter.thy src/HOL/Hyperreal/Integration.thy src/HOL/IsaMakefile

2004-07-30 paulson [Fri, 30 Jul 2004 18:37:58 +0200] rev 15093
conversion of Integration and NSPrimes to Isar scripts
src/HOL/Complex/ex/NSPrimes.ML src/HOL/Complex/ex/NSPrimes.thy src/HOL/Hyperreal/Integration.ML src/HOL/Hyperreal/Integration.thy src/HOL/IsaMakefile src/HOL/OrderedGroup.thy

2004-07-30 wenzelm [Fri, 30 Jul 2004 10:44:42 +0200] rev 15092
keep type_solver;
src/ZF/simpdata.ML

2004-07-30 wenzelm [Fri, 30 Jul 2004 10:44:34 +0200] rev 15091
tuned dependencies;
src/ZF/upair.thy

2004-07-30 wenzelm [Fri, 30 Jul 2004 10:44:27 +0200] rev 15090
added context type solver;
src/ZF/Tools/typechk.ML

2004-07-30 wenzelm [Fri, 30 Jul 2004 10:42:19 +0200] rev 15089
ZF/Simplifier: second copy of context type solver;
NEWS

2004-07-30 wenzelm [Fri, 30 Jul 2004 10:41:52 +0200] rev 15088
tuned output;
src/Pure/meta_simplifier.ML

2004-07-29 berghofe [Thu, 29 Jul 2004 17:45:21 +0200] rev 15087
- optimized nodup_vars check in capply
- new function dest_ctyp
src/Pure/thm.ML

2004-07-29 paulson [Thu, 29 Jul 2004 16:57:41 +0200] rev 15086
removal of more iff-rules from RealDef.thy
src/HOL/Hyperreal/Lim.thy src/HOL/Hyperreal/Transcendental.thy src/HOL/Real/RealDef.thy