| Fri, 10 Aug 2012 21:53:20 +0200 | wenzelm | more precise recover_quoted, recover_verbatim, recover_comment (cf. ML version) -- NB: context parsers expect explicit termination; | changeset | files |
| Fri, 10 Aug 2012 21:22:40 +0200 | wenzelm | tuned message; | changeset | files |
| Fri, 10 Aug 2012 20:53:16 +0200 | wenzelm | clarified Linear_Set.next/prev: check definedness; | changeset | files |
| Fri, 10 Aug 2012 18:03:46 +0200 | nipkow | merged | changeset | files |