Re: [isabelle-dev] text_fold

2014-02-10 Thread Dmitriy Traytel
Am 10.02.2014 14:18, schrieb Makarius: On Mon, 25 Nov 2013, Dmitriy Traytel wrote: Am 23.11.2013 19:42, schrieb Makarius: On Mon, 28 Oct 2013, Dmitriy Traytel wrote: Concerning the error messages: at least you should always get strictly more information than without coercion inference

Re: [isabelle-dev] Shadowing of theorem names in locales

2014-02-10 Thread Makarius
On Fri, 10 Jan 2014, Clemens Ballarin wrote: This does not exhibit itself until the compromised locale context is (re-)entered, and I think this is not desirable. My first spontaneous thought is that strictness should not apply during the initialisation of a locale context. I wouldn't want

[isabelle-dev] underscore in latex

2014-02-10 Thread Makarius
Some notes on that notoriously difficult topic. Classically the T1 encoding allows to get some actual (searchable) underscore characters, depending on fonts. See also changeset: 55295:3951ced4156c user:blanchet date:Mon Feb 03 17:55:50 2014 +0100 files: