| Sat, 16 Jul 2011 00:01:17 +0200 | Cezary Kaliszyk | HOL/Import: Fix errors with _mk_list | changeset | files |
| Fri, 15 Jul 2011 16:51:01 +0200 | wenzelm | Element.activate: leave check of binding where actually applied to the context -- allow internal qualifications, or non-identifier fact names like "assumes *: A" (see also 1183951365de); | changeset | files |
| Fri, 15 Jul 2011 14:07:12 +0200 | wenzelm | simplified malformed YXML markup -- special controls are visible in IsabelleText font; | changeset | files |
| Fri, 15 Jul 2011 13:29:00 +0200 | wenzelm | less ambitious ProofGeneral markup, which occasionally breaks plain-old regexps in elisp; | changeset | files |
| Fri, 15 Jul 2011 13:28:16 +0200 | wenzelm | more robust Binding.pretty/print in typical error sitations with spaces etc. (NB: markup can only provide *additional* emphasis and is occasionally suppressed in TTY mode or tooltips); | changeset | files |
| Fri, 15 Jul 2011 00:49:38 +0200 | wenzelm | more visible printing of empty binding; | changeset | files |