| Wed, 17 Aug 2011 11:39:09 -0700 | huffman | add lemma tendsto_compose_eventually; use it to shorten some proofs | changeset | files |
| Wed, 17 Aug 2011 11:07:32 -0700 | huffman | Topology_Euclidean_Space.thy: simplify some proofs | changeset | files |
| Wed, 17 Aug 2011 11:06:39 -0700 | huffman | add lemma metric_tendsto_imp_tendsto | changeset | files |
| Wed, 17 Aug 2011 09:59:10 -0700 | huffman | simplify proofs of lemmas open_interval, closed_interval | changeset | files |
| Wed, 17 Aug 2011 23:37:23 +0200 | wenzelm | identify parallel exceptions where they emerge first -- to achieve unique results within evaluation graph; | changeset | files |
| Wed, 17 Aug 2011 22:25:00 +0200 | wenzelm | clarified Par_Exn.release_first: traverse topmost list structure only, not arbitrary depths of nested Par_Exn; | changeset | files |
| Wed, 17 Aug 2011 22:14:22 +0200 | wenzelm | more systematic handling of parallel exceptions; | changeset | files |