2010-10-15 Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 15 Oct 2010 21:50:26 +0900] rev 39996
FSet: definition changes propagated from Nominal and more use of 'descending' tactic
src/HOL/Quotient_Examples/FSet.thy

2010-10-15 Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 15 Oct 2010 21:47:45 +0900] rev 39995
FSet tuned
src/HOL/Quotient_Examples/FSet.thy

2010-10-15 Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 15 Oct 2010 21:46:45 +0900] rev 39994
FSet: give names to respectfulness theorems, rename list_all2_refl to avoid clash
src/HOL/Quotient_Examples/FSet.thy

2010-10-14 krauss [Thu, 14 Oct 2010 12:40:14 +0200] rev 39993
NEWS
NEWS

2010-10-10 krauss [Sun, 10 Oct 2010 22:50:25 +0200] rev 39992
removed output syntax "'a ~=> 'b" for "'a => 'b option"
src/HOL/Map.thy

2010-10-13 krauss [Wed, 13 Oct 2010 09:56:00 +0200] rev 39991
reactivated
src/ZF/ex/misc.thy

2010-10-12 krauss [Tue, 12 Oct 2010 21:30:44 +0200] rev 39990
slightly more robust proof
src/HOL/Algebra/Lattice.thy

2010-10-11 huffman [Mon, 11 Oct 2010 08:32:09 -0700] rev 39989
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
src/HOLCF/Algebraic.thy src/HOLCF/Bifinite.thy src/HOLCF/ConvexPD.thy src/HOLCF/Library/Strict_Fun.thy src/HOLCF/LowerPD.thy src/HOLCF/Powerdomains.thy src/HOLCF/Representable.thy src/HOLCF/Tools/Domain/domain_isomorphism.ML src/HOLCF/Tools/repdef.ML src/HOLCF/UpperPD.thy src/HOLCF/ex/Domain_Proofs.thy

2010-10-11 huffman [Mon, 11 Oct 2010 07:09:42 -0700] rev 39988
merged

2010-10-09 huffman [Sat, 09 Oct 2010 07:24:49 -0700] rev 39987
move all bifinite class instances to Bifinite.thy
src/HOLCF/Bifinite.thy src/HOLCF/Cprod.thy src/HOLCF/Lift.thy src/HOLCF/Representable.thy src/HOLCF/Sprod.thy src/HOLCF/Ssum.thy src/HOLCF/Up.thy