| Tue, 14 Jul 2015 11:29:43 +0200 | wenzelm | normalize proof before splitting conjunctions, according to Proof.conclude_goal (see also 4dd0ba632e40) -- may reduce general resource usage; | changeset | files |
| Tue, 14 Jul 2015 13:48:03 +0200 | hoelzl | generalized filtermap_homeomorph to filtermap_fun_inverse; add eventually_at_top/bot_not_equal | changeset | files |
| Tue, 14 Jul 2015 13:37:44 +0200 | hoelzl | add continuous_onI_mono | changeset | files |