Tue, 06 Aug 2013 15:50:23 +0200 | blanchet | tuning | changeset | files |
Tue, 06 Aug 2013 15:50:23 +0200 | blanchet | export ML function (for primcorec) | changeset | files |
Mon, 05 Aug 2013 21:23:06 +0200 | wenzelm | more central Pretty_Tooltip.dismissed_all -- avoid spurious crash of Rich_Text_Area.robust_body in asynchronous mouse_motion_listener; | changeset | files |
Mon, 05 Aug 2013 17:52:07 +0200 | wenzelm | tuned proofs; | changeset | files |