2009-08-26 nipkow [Wed, 26 Aug 2009 19:54:01 +0200] rev 32415
got rid of complicated class finite_intvl_succ and defined "upto" directly on int, the only instance of the class.
src/HOL/GCD.thy src/HOL/List.thy

2009-08-26 chaieb [Wed, 26 Aug 2009 17:38:18 +0100] rev 32414
merged

2009-08-26 chaieb [Wed, 26 Aug 2009 17:38:02 +0100] rev 32413
merged
src/HOL/Library/Formal_Power_Series.thy

2009-08-26 chaieb [Wed, 26 Aug 2009 17:34:32 +0100] rev 32412
removed unused theorem finite_Atleast_Atmost
src/HOL/Library/Euclidean_Space.thy

2009-05-19 chaieb [Tue, 19 May 2009 14:13:37 +0100] rev 32411
merged
src/HOL/Library/Formal_Power_Series.thy

2009-05-19 chaieb [Tue, 19 May 2009 14:13:23 +0100] rev 32410
Derivative of general reverses
src/HOL/Library/Formal_Power_Series.thy

2009-08-26 nipkow [Wed, 26 Aug 2009 16:41:37 +0200] rev 32409
merged

2009-08-26 nipkow [Wed, 26 Aug 2009 16:13:19 +0200] rev 32408
new interval lemma
CCS example for predicate compiler
src/HOL/SetInterval.thy src/HOL/ex/Predicate_Compile_ex.thy

2009-08-26 paulson [Wed, 26 Aug 2009 12:52:01 +0100] rev 32407
merged

2009-08-26 paulson [Wed, 26 Aug 2009 12:51:38 +0100] rev 32406
Simplified some proofs using metis.
src/HOL/Auth/Kerberos_BAN.thy