2003-12-23 paulson [Tue, 23 Dec 2003 14:45:47 +0100] rev 14320
tidying up hcomplex arithmetic
src/HOL/Complex/CLim.ML src/HOL/Complex/NSCA.ML src/HOL/Complex/NSCA.thy src/HOL/Complex/NSComplex.thy src/HOL/Complex/NSComplexArith0.ML src/HOL/Complex/NSComplexArith0.thy src/HOL/Complex/NSComplexBin.ML src/HOL/IsaMakefile

2003-12-23 paulson [Tue, 23 Dec 2003 14:45:23 +0100] rev 14319
renaming some theorems
src/HOL/Hyperreal/NthRoot.ML src/HOL/Hyperreal/SEQ.ML

2003-12-23 paulson [Tue, 23 Dec 2003 12:54:45 +0100] rev 14318
type hcomplex is now in class field
src/HOL/Complex/CLim.ML src/HOL/Complex/NSCA.ML src/HOL/Complex/NSComplex.thy src/HOL/Complex/NSComplexArith0.ML src/HOL/Complex/NSComplexBin.ML

2003-12-23 paulson [Tue, 23 Dec 2003 12:54:15 +0100] rev 14317
more ML bindings
src/HOL/Real/RealOrd.thy src/HOL/Real/real_arith.ML

2003-12-23 kleing [Tue, 23 Dec 2003 06:35:41 +0100] rev 14316
added some [intro?] and [trans] for list_all2 lemmas
src/HOL/List.thy

2003-12-22 nipkow [Mon, 22 Dec 2003 22:52:38 +0100] rev 14315
Updated proofs due to changes in Set.thy.
src/HOL/HoareParallel/RG_Hoare.thy

2003-12-22 paulson [Mon, 22 Dec 2003 18:29:20 +0100] rev 14314
converted Complex/NSComplex to Isar script
src/HOL/Complex/NSComplex.ML src/HOL/Complex/NSComplex.thy src/HOL/IsaMakefile

2003-12-22 paulson [Mon, 22 Dec 2003 16:22:14 +0100] rev 14313
removal of the abel_cancel simproc for hypreal
src/HOL/Hyperreal/HyperBin.ML src/HOL/Hyperreal/HyperOrd.thy

2003-12-22 paulson [Mon, 22 Dec 2003 15:42:21 +0100] rev 14312
downgrading abel_cancel
src/HOL/Hyperreal/HyperOrd.thy

2003-12-22 paulson [Mon, 22 Dec 2003 15:41:25 +0100] rev 14311
new binding
src/HOL/Complex/NSComplex.ML src/HOL/Real/real_arith.ML