2001-10-05 wenzelm [Fri, 05 Oct 2001 23:58:52 +0200] rev 11703
tuned;
src/HOL/TLA/Action.thy src/HOL/TLA/Inc/Inc.thy src/HOL/TLA/Inc/Pcount.thy src/HOL/TLA/Inc/ROOT.ML src/HOL/TLA/Init.thy src/HOL/TLA/Memory/MIParameters.thy src/HOL/TLA/Memory/MemClerk.thy src/HOL/TLA/Memory/MemClerkParameters.thy src/HOL/TLA/Memory/Memory.thy src/HOL/TLA/Memory/MemoryImplementation.thy src/HOL/TLA/Memory/ProcedureInterface.thy src/HOL/TLA/Memory/RPC.thy src/HOL/TLA/Memory/RPCMemoryParams.thy src/HOL/TLA/Memory/RPCParameters.thy src/HOL/TLA/Stfun.thy

2001-10-05 wenzelm [Fri, 05 Oct 2001 23:58:17 +0200] rev 11702
*** empty log message ***
NEWS

2001-10-05 wenzelm [Fri, 05 Oct 2001 21:52:39 +0200] rev 11701
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
"num" syntax (still with "#"), Numeral0, Numeral1;
src/HOL/Algebra/poly/PolyHomo.ML src/HOL/Auth/KerberosIV.thy src/HOL/Auth/Kerberos_BAN.thy src/HOL/Datatype_Universe.ML src/HOL/Datatype_Universe.thy src/HOL/Divides.ML src/HOL/Finite.ML src/HOL/GroupTheory/Exponent.ML src/HOL/Hoare/Arith2.ML src/HOL/Hoare/Examples.ML src/HOL/Hyperreal/HRealAbs.ML src/HOL/Hyperreal/HSeries.ML src/HOL/Hyperreal/HyperArith0.ML src/HOL/Hyperreal/HyperBin.ML src/HOL/Hyperreal/HyperDef.ML src/HOL/Hyperreal/HyperDef.thy src/HOL/Hyperreal/HyperNat.ML src/HOL/Hyperreal/HyperOrd.ML src/HOL/Hyperreal/HyperPow.ML src/HOL/Hyperreal/Lim.ML src/HOL/Hyperreal/Lim.thy src/HOL/Hyperreal/NSA.ML src/HOL/Hyperreal/NatStar.ML src/HOL/Hyperreal/SEQ.ML src/HOL/Hyperreal/SEQ.thy src/HOL/Hyperreal/Series.ML src/HOL/Hyperreal/Series.thy src/HOL/Hyperreal/hypreal_arith0.ML src/HOL/IMP/Compiler.thy src/HOL/IMP/Examples.ML src/HOL/IMPP/EvenOdd.ML src/HOL/IMPP/EvenOdd.thy src/HOL/Induct/Com.thy src/HOL/Induct/Mutil.thy src/HOL/Integ/Bin.ML src/HOL/Integ/Int.ML src/HOL/Integ/IntArith.ML src/HOL/Integ/IntDef.ML src/HOL/Integ/IntDef.thy src/HOL/Integ/IntDiv.ML src/HOL/Integ/IntDiv.thy src/HOL/Integ/IntPower.ML src/HOL/Integ/IntPower.thy src/HOL/Integ/NatSimprocs.ML src/HOL/Integ/int_arith1.ML src/HOL/Integ/int_arith2.ML src/HOL/Integ/int_factor_simprocs.ML src/HOL/Integ/nat_bin.ML src/HOL/Integ/nat_simprocs.ML src/HOL/Isar_examples/Fibonacci.thy ...

2001-10-05 wenzelm [Fri, 05 Oct 2001 21:50:37 +0200] rev 11700
*** empty log message ***
NEWS

2001-10-05 wenzelm [Fri, 05 Oct 2001 21:49:59 +0200] rev 11699
"num" syntax;
src/HOL/Numeral.ML src/HOL/Numeral.thy

2001-10-05 wenzelm [Fri, 05 Oct 2001 21:49:15 +0200] rev 11698
added axclass "one" and polymorphic const "1";
print consts "0" and "1" with type constraints;
src/HOL/HOL.thy

2001-10-05 wenzelm [Fri, 05 Oct 2001 21:48:04 +0200] rev 11697
added "num" token;
src/Pure/Syntax/lexicon.ML src/Pure/Syntax/token_trans.ML

2001-10-05 wenzelm [Fri, 05 Oct 2001 21:42:10 +0200] rev 11696
induct: case names;
src/FOL/ex/Natural_Numbers.thy

2001-10-05 wenzelm [Fri, 05 Oct 2001 21:37:33 +0200] rev 11695
sane spacing of "-";
src/ZF/equalities.ML src/ZF/simpdata.ML

2001-10-05 wenzelm [Fri, 05 Oct 2001 16:04:56 +0200] rev 11694
tuned;
src/ZF/pair.thy