2002-05-31 nipkow [Fri, 31 May 2002 07:53:37 +0200] rev 13189
Now arith can deal with div/mod arbitrary nat numerals.
src/HOL/Divides.thy src/HOL/Integ/NatBin.thy

2002-05-30 nipkow [Thu, 30 May 2002 10:21:28 +0200] rev 13188
*** empty log message ***
NEWS

2002-05-30 nipkow [Thu, 30 May 2002 10:12:52 +0200] rev 13187
Modifications due to enhanced linear arithmetic.
src/HOL/Hoare/Examples.ML src/HOL/HoareParallel/Gar_Coll.thy src/HOL/HoareParallel/Mul_Gar_Coll.thy src/HOL/HoareParallel/OG_Examples.thy src/HOL/HoareParallel/OG_Tactics.thy src/HOL/HoareParallel/RG_Examples.thy src/HOL/HoareParallel/RG_Hoare.thy src/HOL/HoareParallel/RG_Tran.thy src/HOL/Hyperreal/MacLaurin.ML src/HOL/Integ/IntArith.ML src/HOL/Isar_examples/MutilatedCheckerboard.thy src/HOL/Lambda/Eta.thy src/HOL/Lambda/Lambda.thy src/HOL/Lex/RegSet_of_nat_DA.ML src/HOL/Library/Primes.thy src/HOL/List.thy src/HOL/MicroJava/BV/BVExample.thy src/HOL/NumberTheory/Chinese.thy src/HOL/NumberTheory/EulerFermat.thy src/HOL/NumberTheory/IntPrimes.thy src/HOL/NumberTheory/WilsonRuss.thy src/HOL/TLA/TLA.ML src/HOL/ex/AVL.ML src/HOL/ex/BinEx.thy

2002-05-30 nipkow [Thu, 30 May 2002 10:12:11 +0200] rev 13186
Big update. Allows case splitting on ~= now (trying both < and >).
src/Provers/Arith/fast_lin_arith.ML

2002-05-28 paulson [Tue, 28 May 2002 11:07:36 +0200] rev 13185
deleted some useless ML bindings
src/ZF/Arith.thy src/ZF/Epsilon.thy src/ZF/Nat.thy src/ZF/Order.thy src/ZF/OrderType.thy src/ZF/Perm.thy src/ZF/Univ.thy

2002-05-28 paulson [Tue, 28 May 2002 11:06:55 +0200] rev 13184
added <-> and ~
lib/scripts/unsymbolize.pl

2002-05-28 paulson [Tue, 28 May 2002 11:06:06 +0200] rev 13183
conversion of IntDiv.thy to Isar format
src/HOL/Integ/IntDiv.ML src/HOL/Integ/IntDiv.thy src/HOL/Integ/nat_bin.ML src/HOL/IsaMakefile src/HOL/NumberTheory/IntPrimes.thy

2002-05-28 berghofe [Tue, 28 May 2002 09:46:39 +0200] rev 13182
Eps -> Hilbert_Choice.Eps
TFL/dcterm.ML TFL/usyntax.ML

2002-05-27 nipkow [Mon, 27 May 2002 17:20:16 +0200] rev 13181
*** empty log message ***
doc-src/TutorialI/Misc/document/natsum.tex doc-src/TutorialI/Misc/natsum.thy

2002-05-24 paulson [Fri, 24 May 2002 16:56:25 +0200] rev 13180
tidied; stronger lemmas about functions
src/ZF/Perm.thy