2004-01-26 schirmer [Mon, 26 Jan 2004 10:34:02 +0100] rev 14361
* Support for raw latex output in control symbols: \<^raw...>
* Symbols may only start with one backslash: \<...>. \\<...> is no longer
accepted by the scanner.
- Adapted some Isar-theories to fit to this policy
NEWS src/HOL/HOL.thy src/HOL/Hyperreal/HyperDef.thy src/HOL/Transitive_Closure.thy src/HOL/UNITY/Comp/AllocBase.thy src/Pure/General/symbol.ML src/Pure/Thy/latex.ML

2004-01-25 nipkow [Sun, 25 Jan 2004 00:42:22 +0100] rev 14360
Added an exception handler and error msg.
src/Provers/Arith/fast_lin_arith.ML

2004-01-20 schirmer [Tue, 20 Jan 2004 13:56:27 +0100] rev 14359
Added print translation for pairs
src/HOL/Product_Type.thy

2004-01-20 schirmer [Tue, 20 Jan 2004 13:55:22 +0100] rev 14358
cleaning up
src/HOL/Tools/record_package.ML

2004-01-14 kleing [Wed, 14 Jan 2004 07:53:27 +0100] rev 14357
print translation for ALL x <= n. P x
doc-src/TutorialI/Types/Overloading2.thy src/HOL/HOL.thy

2004-01-14 nipkow [Wed, 14 Jan 2004 04:41:16 +0100] rev 14356
fixed old bugs in "decomp" (conversion from term to lin.arith. format).
updated instantiation of real lin.arith.
src/HOL/Real/real_arith.ML src/HOL/arith_data.ML

2004-01-14 nipkow [Wed, 14 Jan 2004 00:13:04 +0100] rev 14355
Told linear arithmetic package about injections "real" from nat/int into real.
src/HOL/Hyperreal/IntFloor.ML src/HOL/Hyperreal/NthRoot.thy src/HOL/Hyperreal/SEQ.ML src/HOL/Hyperreal/Transcendental.ML src/HOL/IsaMakefile src/HOL/Real/real_arith.ML

2004-01-13 paulson [Tue, 13 Jan 2004 10:37:52 +0100] rev 14354
types complex and hcomplex are now instances of class ringpower:
omitting redundant lemmas
src/HOL/Complex/CLim.ML src/HOL/Complex/Complex.thy src/HOL/Complex/NSComplex.thy

2004-01-12 paulson [Mon, 12 Jan 2004 16:51:45 +0100] rev 14353
Added lemmas to Ring_and_Field with slightly modified simplification rules

Deleted some little-used integer theorems, replacing them by the generic ones
in Ring_and_Field

Consolidated integer powers
doc-src/TutorialI/Documents/Documents.thy doc-src/TutorialI/Documents/document/Documents.tex doc-src/TutorialI/Types/Numbers.thy doc-src/TutorialI/Types/document/Numbers.tex doc-src/TutorialI/Types/document/Records.tex doc-src/TutorialI/Types/numerics.tex doc-src/TutorialI/isabelle.sty src/HOL/Complex/Complex.thy src/HOL/Complex/NSCA.ML src/HOL/Complex/NSComplexBin.ML src/HOL/Complex/ex/Sqrt.thy src/HOL/Hoare/Arith2.ML src/HOL/Integ/Int.thy src/HOL/Integ/IntArith.thy src/HOL/Integ/IntDiv.thy src/HOL/Integ/IntPower.thy src/HOL/Integ/NatBin.thy src/HOL/Integ/NatSimprocs.thy src/HOL/Integ/Presburger.thy src/HOL/Integ/presburger.ML src/HOL/IsaMakefile src/HOL/Library/Primes.thy src/HOL/Library/Rational_Numbers.thy src/HOL/NumberTheory/Chinese.thy src/HOL/NumberTheory/Gauss.thy src/HOL/NumberTheory/IntPrimes.thy src/HOL/NumberTheory/Quadratic_Reciprocity.thy src/HOL/Power.thy src/HOL/Presburger.thy src/HOL/Ring_and_Field.thy src/HOL/Tools/Presburger/presburger.ML src/HOL/ex/PresburgerEx.thy src/HOL/ex/set.thy

2004-01-12 paulson [Mon, 12 Jan 2004 16:45:35 +0100] rev 14352
Modified real arithmetic simplification
src/HOL/Hyperreal/HyperArith.thy src/HOL/Hyperreal/HyperArith0.thy src/HOL/Hyperreal/HyperBin.ML src/HOL/Hyperreal/Transcendental.ML src/HOL/Hyperreal/hypreal_arith.ML src/HOL/Hyperreal/hypreal_arith0.ML src/HOL/Real/Complex_Numbers.thy src/HOL/Real/RealArith.thy src/HOL/Real/RealArith0.thy src/HOL/Real/RealBin.ML src/HOL/Real/RealPow.thy src/HOL/Real/real_arith.ML src/HOL/Real/real_arith0.ML