Re: [isabelle] Isabelle2016-RC0 - text with cartouches outside theory

On 19/10/16 21:12, JÃrgen Villadsen wrote:
> In HOL/ex/ML.thy, moving the following line before the theory command gives an error message, but why?
> text âSee ðââ.â;

Before the 'theory' command there is no formal context, but
antiquotations (like the globe for @{url}) always require that.

> By the way, is there a short expression for the following line used in the Scala console for batch processing?
>, select_dirs = List(Path.explode("~/Documents")))

Mine is even longer, because I usually include (new Console_Progress) in
the expression.

I usually use the persistent Console history to get back to older

The document system is awaiting a great renovation and full integration
into the Prover IDE (at least since 2013).


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.