2007-12-18 haftmann [Tue, 18 Dec 2007 14:37:00 +0100] rev 25691
switched from PreList to ATP_Linkup
src/HOL/Library/Binomial.thy src/HOL/Library/Boolean_Algebra.thy src/HOL/Library/Code_Index.thy src/HOL/Library/Continuity.thy src/HOL/Library/Eval.thy src/HOL/Library/NatPair.thy src/HOL/Library/Nat_Infinity.thy src/HOL/Library/Parity.thy src/HOL/Library/Product_ord.thy src/HOL/Library/Quotient.thy src/HOL/Library/Ramsey.thy src/HOL/Library/SetsAndFunctions.thy src/HOL/Library/Zorn.thy

2007-12-18 berghofe [Tue, 18 Dec 2007 12:26:24 +0100] rev 25690
Renamed *.size to prod.size.
src/HOL/Nat.thy

2007-12-18 berghofe [Tue, 18 Dec 2007 12:26:00 +0100] rev 25689
Alternative names are now also used when storing theorems for
size functions.
src/HOL/Tools/function_package/size.ML

2007-12-18 krauss [Tue, 18 Dec 2007 11:45:08 +0100] rev 25688
temporarily fixed documentation due to changed size functions
doc-src/IsarAdvanced/Functions/Thy/Functions.thy

2007-12-18 wenzelm [Tue, 18 Dec 2007 00:17:00 +0100] rev 25687
split_primel: salvaged original proof after blow with sledghammer
(this constructive version is required in HOL/Extraction);
src/HOL/Extraction/Euclid.thy src/HOL/NumberTheory/Factorization.thy

2007-12-17 wenzelm [Mon, 17 Dec 2007 23:33:00 +0100] rev 25686
cond_timeit: added message argument, use Exn.capture/release;
tuned;
src/Pure/General/output.ML

2007-12-17 wenzelm [Mon, 17 Dec 2007 23:26:27 +0100] rev 25685
cond_timeit: added message argument;
src/Pure/Isar/outer_syntax.ML src/Pure/old_goals.ML

2007-12-17 haftmann [Mon, 17 Dec 2007 22:40:14 +0100] rev 25684
note in target
src/Pure/Isar/theory_target.ML

2007-12-17 haftmann [Mon, 17 Dec 2007 22:40:13 +0100] rev 25683
maior tuning
src/Pure/Isar/class.ML

2007-12-17 haftmann [Mon, 17 Dec 2007 22:40:12 +0100] rev 25682
tuned
src/Pure/General/output.ML