2012-05-08 bulwahn [Tue, 08 May 2012 14:35:13 +0200] rev 47894
defining and proving Executable_Relation with lift_definition and transfer
src/HOL/ex/Executable_Relation.thy

2012-05-08 bulwahn [Tue, 08 May 2012 14:31:03 +0200] rev 47893
specialised fact in the Record theory should not be appear in proofs discovered by sledgehammer
src/HOL/Record.thy

2012-05-07 blanchet [Mon, 07 May 2012 14:50:49 +0200] rev 47892
prevent spurious timeouts
src/HOL/Metis_Examples/Proxies.thy

2012-05-07 blanchet [Mon, 07 May 2012 12:20:55 +0200] rev 47891
added "try0" tool to Mirabelle
src/HOL/Mirabelle/Mirabelle_Test.thy src/HOL/Mirabelle/Tools/mirabelle_try0.ML

2012-05-07 blanchet [Mon, 07 May 2012 12:20:55 +0200] rev 47890
use latest E (1.5)
Admin/contributed_components

2012-05-04 huffman [Fri, 04 May 2012 17:12:37 +0200] rev 47889
lifting package produces abs_eq_iff rules for total quotients
src/HOL/Lifting.thy src/HOL/Tools/Lifting/lifting_setup.ML

2012-05-04 bulwahn [Fri, 04 May 2012 11:08:31 +0200] rev 47888
using the new transfer method to obtain abstract properties of RBT trees
src/HOL/Quotient_Examples/Lift_RBT.thy

2012-05-02 wenzelm [Wed, 02 May 2012 22:05:59 +0200] rev 47887
back to post-release mode -- after fork point;
Admin/makedist CONTRIBUTORS NEWS

2012-05-23 wenzelm [Wed, 23 May 2012 11:53:17 +0200] rev 47886
removed obsolete RC tags;
.hgtags

2012-05-22 wenzelm [Tue, 22 May 2012 19:02:17 +0200] rev 47885
Added tag Isabelle2012 for changeset 21c42b095c84
.hgtags