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

2001-08-06 paulson [Mon, 06 Aug 2001 15:46:20 +0200] rev 11465
Changed 1 to 1' (= Suc 0)
src/HOL/Auth/KerberosIV.thy src/HOL/Auth/Kerberos_BAN.thy src/HOL/Auth/NS_Shared.thy

2001-08-06 nipkow [Mon, 06 Aug 2001 13:43:24 +0200] rev 11464
turned translation for 1::nat into def.
introduced 1' and replaced most occurrences of 1 by 1'.
src/HOL/Datatype_Universe.ML src/HOL/Divides.ML src/HOL/Hoare/Examples.ML src/HOL/IMPP/EvenOdd.ML src/HOL/Induct/Com.thy src/HOL/Induct/Mutil.thy src/HOL/Integ/IntDef.ML src/HOL/Integ/NatBin.thy src/HOL/Integ/NatSimprocs.ML src/HOL/Integ/nat_bin.ML src/HOL/Isar_examples/Fibonacci.thy src/HOL/Library/Multiset.thy src/HOL/Library/Primes.thy src/HOL/Nat.ML src/HOL/NatDef.ML src/HOL/NatDef.thy src/HOL/Power.ML src/HOL/Real/PNat.ML src/HOL/Real/PNat.thy src/HOL/Real/PRat.ML src/HOL/Real/PReal.ML src/HOL/Real/RealOrd.ML src/HOL/arith_data.ML src/HOL/ex/Primrec.thy

2001-08-06 paulson [Mon, 06 Aug 2001 13:12:06 +0200] rev 11463
three new theorems
src/HOL/Auth/Event.thy

2001-08-06 paulson [Mon, 06 Aug 2001 12:46:21 +0200] rev 11462
removed the warning from [iff]
src/Provers/clasimp.ML

2001-08-06 paulson [Mon, 06 Aug 2001 12:42:43 +0200] rev 11461
removed an unsuitable default simprule
src/HOL/Library/Continuity.thy src/HOL/NatDef.ML