| Fri, 01 Aug 2014 15:08:49 +0200 | blanchet | careful when calling 'Thm.proof_body_of' -- it can throw exceptions | changeset | files |
| Fri, 01 Aug 2014 20:43:23 +0200 | wenzelm | removed unused stuff; | changeset | files |
| Fri, 01 Aug 2014 20:20:17 +0200 | wenzelm | agree on keyword categories with ML; | changeset | files |
| Fri, 01 Aug 2014 20:15:00 +0200 | wenzelm | more keyword categories (as in ML); | changeset | files |
| Thu, 31 Jul 2014 22:02:21 +0200 | wenzelm | prefer dynamic ML_print_depth if context happens to be available; | changeset | files |
| Thu, 31 Jul 2014 21:29:31 +0200 | wenzelm | completion popup supports both ENTER and TAB (default); | changeset | files |
| Thu, 31 Jul 2014 20:59:10 +0200 | wenzelm | clarified compile-time use of ML_print_depth; | changeset | files |