2004-02-11 nipkow [Wed, 11 Feb 2004 01:26:15 +0100] rev 14381
Modified UN and INT xsymbol syntax: made index subscript
src/HOL/Set.thy

2004-02-11 nipkow [Wed, 11 Feb 2004 00:37:18 +0100] rev 14380
*** empty log message ***
NEWS

2004-02-10 paulson [Tue, 10 Feb 2004 12:17:04 +0100] rev 14379
updated links to the old ftp site
Admin/page/dist-content/docs.content Admin/page/dist-content/past.content Admin/page/main-content/index.content doc-src/ERRATA.txt doc-src/TutorialI/Advanced/document/Partial.tex doc-src/TutorialI/CTL/document/CTL.tex doc-src/TutorialI/CTL/document/CTLind.tex doc-src/TutorialI/CTL/document/PDL.tex doc-src/TutorialI/Documents/document/Documents.tex doc-src/TutorialI/Inductive/document/AB.tex doc-src/TutorialI/Inductive/document/Advanced.tex doc-src/TutorialI/Inductive/document/Star.tex doc-src/TutorialI/Misc/document/AdvancedInd.tex doc-src/TutorialI/Types/document/Overloading2.tex doc-src/TutorialI/Types/document/Records.tex doc-src/manual.bib doc-src/preface.tex

2004-02-10 paulson [Tue, 10 Feb 2004 12:02:11 +0100] rev 14378
generic of_nat and of_int functions, and generalization of iszero
and neg
src/HOL/Complex/CStar.ML src/HOL/Complex/ComplexBin.ML src/HOL/Complex/NSComplexBin.ML src/HOL/Complex/NSInduct.ML src/HOL/Complex/ex/NSPrimes.ML src/HOL/Hyperreal/HSeries.ML src/HOL/Hyperreal/HTranscendental.ML src/HOL/Hyperreal/HyperArith.thy src/HOL/Hyperreal/HyperDef.thy src/HOL/Hyperreal/HyperNat.thy src/HOL/Hyperreal/HyperPow.thy src/HOL/Hyperreal/NSA.thy src/HOL/Hyperreal/NatStar.ML src/HOL/Hyperreal/SEQ.ML src/HOL/Hyperreal/Star.thy src/HOL/Integ/Bin.thy src/HOL/Integ/Int.thy src/HOL/Integ/IntArith.thy src/HOL/Integ/IntDef.thy src/HOL/Integ/IntDiv.thy src/HOL/Integ/NatBin.thy src/HOL/Integ/NatSimprocs.thy src/HOL/Integ/Presburger.thy src/HOL/Integ/int_arith1.ML src/HOL/Integ/int_factor_simprocs.ML src/HOL/IsaMakefile src/HOL/Isar_examples/document/root.bib src/HOL/NumberTheory/IntPrimes.thy src/HOL/Presburger.thy src/HOL/Real/PReal.thy src/HOL/Real/RatArith.thy src/HOL/Real/Rational.thy src/HOL/Real/RealArith.thy src/HOL/Real/RealDef.thy src/HOL/Real/rat_arith.ML src/HOL/UNITY/Simple/Lift.thy src/HOL/ex/BinEx.thy

2004-02-05 paulson [Thu, 05 Feb 2004 10:45:28 +0100] rev 14377
tidying up, especially the Complex numbers
src/HOL/Complex/CStar.ML src/HOL/Complex/Complex.thy src/HOL/Complex/ComplexBin.ML src/HOL/Complex/NSCA.ML src/HOL/Complex/NSComplex.thy src/HOL/Complex/NSComplexBin.ML src/HOL/Real/PReal.thy src/HOL/Ring_and_Field.thy

2004-02-05 nipkow [Thu, 05 Feb 2004 04:30:38 +0100] rev 14376
Changed variable names.
src/HOL/Map.thy

2004-02-04 nipkow [Wed, 04 Feb 2004 03:44:05 +0100] rev 14375
*** empty log message ***
NEWS

2004-02-03 paulson [Tue, 03 Feb 2004 15:58:31 +0100] rev 14374
further tidying of the complex numbers
src/HOL/Complex/Complex.thy src/HOL/Complex/NSCA.ML src/HOL/Complex/NSComplex.thy src/HOL/Real/Complex_Numbers.thy src/HOL/Real/Real.thy

2004-02-03 paulson [Tue, 03 Feb 2004 11:06:36 +0100] rev 14373
tidying of the complex numbers
src/HOL/Complex/CLim.ML src/HOL/Complex/CSeries.ML src/HOL/Complex/Complex.thy src/HOL/Complex/ComplexArith0.ML src/HOL/Complex/ComplexBin.ML src/HOL/Complex/NSCA.ML src/HOL/Complex/NSComplex.thy src/HOL/Complex/NSComplexBin.ML src/HOL/Complex/ex/BinEx.thy src/HOL/IsaMakefile

2004-02-03 nipkow [Tue, 03 Feb 2004 10:19:21 +0100] rev 14372
Finally fixed the counterexample finder. Can now deal with < on real.
src/Provers/Arith/fast_lin_arith.ML