Email Gateway (Aug 22 2022 at 14:18): Email Gateway (Aug 22 2022 at 14:18):From: Jørgen Villadsen <jovi@dtu.dk>
Hi,
In HOL/ex/ML.thy, moving the following line before the theory command gives an error message, but why?
text ‹See 🌐‹http://mathworld.wolfram.com/AckermannFunction.html›.›
By the way, is there a short expression for the following line used in the Scala console for batch processing?
Build.build(Options.init, select_dirs = List(Path.explode("~/Documents")))
Thanks,
Jørgen
Email Gateway (Aug 22 2022 at 14:18):From: Makarius <makarius@sketis.net>
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 🌐‹http://mathworld.wolfram.com/AckermannFunction.html›.›
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?
Build.build(Options.init, 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
invocations.
The document system is awaiting a great renovation and full integration
into the Prover IDE (at least since 2013).
Makarius
Email Gateway (Aug 22 2022 at 14:21):From: Jørgen Villadsen <jovi@dtu.dk>
Thanks for the explanations. I am looking forward to the renovated document system but in the meantime a short expression would be great, something like:
Build.dummy("~/Documents")
By the ways, MikTeX produces the following warning:
Package hyperref Warning: Option `pagecolor' is not available anymore.
Jørgen
-----Original Message-----
From: Makarius [mailto:makarius@sketis.net]
Sent: 19. oktober 2016 23:50
To: Jørgen Villadsen; cl-isabelle-users@lists.cam.ac.uk
Subject: 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 🌐‹http://mathworld.wolfram.com/AckermannFunction.html›.›
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?
Build.build(Options.init, 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 invocations.
The document system is awaiting a great renovation and full integration into the Prover IDE (at least since 2013).
Makarius
Last updated: Nov 21 2024 at 12:39 UTC