2001-08-07 wenzelm [Tue, 07 Aug 2001 22:42:22 +0200] rev 11475
tuned;
NEWS

2001-08-07 wenzelm [Tue, 07 Aug 2001 22:41:46 +0200] rev 11474
tuned;
NEWS

2001-08-07 wenzelm [Tue, 07 Aug 2001 22:37:30 +0200] rev 11473
fix problem with user translations by making field names appear as consts;
src/HOL/Record.thy src/HOL/Tools/record_package.ML

2001-08-07 wenzelm [Tue, 07 Aug 2001 21:27:00 +0200] rev 11472
tuned;
src/HOL/Real/HahnBanach/FunctionNorm.thy src/HOL/Real/HahnBanach/FunctionOrder.thy src/HOL/Real/HahnBanach/VectorSpace.thy

2001-08-07 berghofe [Tue, 07 Aug 2001 19:29:08 +0200] rev 11471
- Fixed bug in isomorphism proofs (caused by migration from SOME to THE)
- Funs_rangeE now requires function g to be injective
src/HOL/Tools/datatype_rep_proofs.ML

2001-08-07 berghofe [Tue, 07 Aug 2001 19:26:42 +0200] rev 11470
Eliminated dependency of Funs_rangeE on SOME.
src/HOL/Datatype_Universe.ML

2001-08-07 oheimb [Tue, 07 Aug 2001 17:21:58 +0200] rev 11469
removed the warning from [iff]
doc-src/IsarRef/generic.tex

2001-08-07 paulson [Tue, 07 Aug 2001 16:36:52 +0200] rev 11468
Tweaks for 1 -> 1'
src/HOL/GroupTheory/Exponent.ML src/HOL/GroupTheory/Sylow.ML src/HOL/GroupTheory/Sylow.thy src/HOL/Hyperreal/HyperNat.ML src/HOL/Hyperreal/HyperPow.ML src/HOL/Hyperreal/Lim.ML src/HOL/Hyperreal/Series.ML src/HOL/Integ/NatBin.thy src/HOL/Integ/NatSimprocs.ML src/HOL/NatArith.ML src/HOL/NumberTheory/Chinese.thy src/HOL/NumberTheory/Factorization.thy src/HOL/NumberTheory/Fib.thy

2001-08-06 paulson [Mon, 06 Aug 2001 16:43:40 +0200] rev 11467
Converted 1 to 1'
src/HOL/UNITY/Extend.ML src/HOL/UNITY/Lift_prog.ML src/HOL/UNITY/Simple/Network.ML src/HOL/UNITY/Simple/Reachability.ML src/HOL/UNITY/Simple/Reachability.thy src/HOL/UNITY/Union.ML

2001-08-06 nipkow [Mon, 06 Aug 2001 15:54:29 +0200] rev 11466
1 -> 1'
src/HOL/MicroJava/BV/Step.thy