2012-10-18 wenzelm [Thu, 18 Oct 2012 19:58:30 +0200] rev 49931
more basic Goal.reset_futures as snapshot of implicit state;
more robust Session.finish_futures: do not cancel here, to allow later Future.map of persistent futures (notably proof terms);
src/Pure/PIDE/protocol.ML src/Pure/System/session.ML src/Pure/goal.ML

2012-10-18 wenzelm [Thu, 18 Oct 2012 19:12:58 +0200] rev 49930
tuned proof;
src/HOL/Isar_Examples/Drinker.thy

2012-10-18 kuncar [Thu, 18 Oct 2012 15:52:33 +0200] rev 49929
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
src/HOL/Library/AList_Mapping.thy src/HOL/Library/Mapping.thy src/HOL/Library/RBT_Mapping.thy src/HOL/ex/Execute_Choice.thy

2012-10-18 kuncar [Thu, 18 Oct 2012 15:52:32 +0200] rev 49928
tuned proofs
src/HOL/Library/RBT_Set.thy

2012-10-18 kuncar [Thu, 18 Oct 2012 15:52:31 +0200] rev 49927
new theorem
src/HOL/Library/RBT.thy

2012-10-18 wenzelm [Thu, 18 Oct 2012 15:47:01 +0200] rev 49926
merged

2012-10-18 wenzelm [Thu, 18 Oct 2012 15:44:14 +0200] rev 49925
merged

2012-10-18 wenzelm [Thu, 18 Oct 2012 15:28:49 +0200] rev 49924
merged

2012-10-18 wenzelm [Thu, 18 Oct 2012 15:16:39 +0200] rev 49923
merged

2012-10-18 wenzelm [Thu, 18 Oct 2012 15:15:08 +0200] rev 49922
fixed proof (cf. a81f95693c68);
src/HOL/Cardinals/Wellorder_Embedding_Base.thy