| Wed, 20 Feb 2013 12:04:42 +0100 | hoelzl | split dense into inner_dense_order and no_top/no_bot | changeset | files |
| Wed, 20 Feb 2013 12:04:42 +0100 | hoelzl | move auxiliary lemmas from Library/Extended_Reals to HOL image | changeset | files |
| Mon, 04 Mar 2013 09:57:54 +0100 | traytel | tuned (extend datatype to inline option) | changeset | files |
| Sun, 03 Mar 2013 18:50:46 +0100 | wenzelm | prefer more systematic Future.flat; | changeset | files |
| Sun, 03 Mar 2013 17:34:42 +0100 | wenzelm | more uniform Future.map: always internalize failure; | changeset | files |
| Sun, 03 Mar 2013 14:29:30 +0100 | wenzelm | uniform treatment of global/local proofs; | changeset | files |
| Sun, 03 Mar 2013 13:57:03 +0100 | wenzelm | tuned; | changeset | files |
| Sun, 03 Mar 2013 13:43:57 +0100 | wenzelm | clarified Toplevel.element_result wrt. Toplevel.is_ignored; | changeset | files |