Am 30/08/2012 22:37, schrieb Makarius:
> On Thu, 30 Aug 2012, Tobias Nipkow wrote:
>
>> I am still having some problems with it. Given
>>
>> session "HOL-IMP1" in "~~/src/HOL/IMP" = HOL +
>> options [document_output="IMP-generated", document=pdf]
>> theories
>>BExp
>>
>> then isabelle build
On Thu, 30 Aug 2012, Tobias Nipkow wrote:
I am still having some problems with it. Given
session "HOL-IMP1" in "~~/src/HOL/IMP" = HOL +
options [document_output="IMP-generated", document=pdf]
theories
BExp
then isabelle build -d . HOL-IMP1 puts IMP-generated into "~~/src/HOL/IMP" - I
gues
On Thu, 30 Aug 2012, Tobias Nipkow wrote:
BTW, the latest version of the logo tool triggers a bug in older
versions of epstopdf:
lapbroy100:Doc nipkow$ isabelle logo -o isabelle.pdf xxx
isabelle.pdf
epstopdf ($Id: epstopdf.pl 15843 2009-10-19 23:14:41Z karl $) 2.11
!!! Error: Cannot open stand
Am 29/08/2012 14:21, schrieb Makarius:
> On Wed, 29 Aug 2012, Gerwin Klein wrote:
>
>> A small annoyance with document_output was that the output doesn't seem to
>> get
>> produced for document=false (i.e. seems to force a latex run) and that it
>> insists on creating a "document" subdirectory in
Am 29/08/2012 14:21, schrieb Makarius:
> On Wed, 29 Aug 2012, Gerwin Klein wrote:
>
>> A small annoyance with document_output was that the output doesn't seem to
>> get
>> produced for document=false (i.e. seems to force a latex run) and that it
>> insists on creating a "document" subdirectory in
On 29/08/2012, at 10:21 PM, Makarius wrote:
> On Wed, 29 Aug 2012, Gerwin Klein wrote:
>
>> A small annoyance with document_output was that the output doesn't seem to
>> get produced for document=false (i.e. seems to force a latex run) and that
>> it insists on creating a "document" subdirect
On Wed, 29 Aug 2012, Gerwin Klein wrote:
A small annoyance with document_output was that the output doesn't seem
to get produced for document=false (i.e. seems to force a latex run) and
that it insists on creating a "document" subdirectory in the target
directory that I give it.
In fact it p
On Wed, 29 Aug 2012, Lawrence Paulson wrote:
This has always been my approach as well. Long ago I wrote a little
script for post-processing the latex files. Larry
On 29 Aug 2012, at 07:16, Gerwin Klein wrote:
I use -D/document_dump extensively for producing papers. The Isabelle
Latex output
This has always been my approach as well. Long ago I wrote a little script for
post-processing the latex files.
Larry
On 29 Aug 2012, at 07:16, Gerwin Klein wrote:
> I use -D/document_dump extensively for producing papers. The Isabelle Latex
> output pretty much always requires post processing
For my most recent locales paper some tex files are generated with
Isabelle 2009-1 because it uses the old axclass interface. The rest
is produced with a current repository version. All files are dumped
to the same document folder. I wonder whether there is any chance to
convert this som
On 08/29/2012 03:16 PM, Gerwin Klein wrote:
On 28/08/2012, at 8:06 PM, Makarius wrote:
Are there remaining uses (or users) of the old document_dump /
document_dump_mode options? This corresponds to former options -D and -C of
isabelle usedir.
The meaning of these features has become quite d
On 28/08/2012, at 8:06 PM, Makarius wrote:
> Are there remaining uses (or users) of the old document_dump /
> document_dump_mode options? This corresponds to former options -D and -C of
> isabelle usedir.
>
> The meaning of these features has become quite difficult to define, so it
> looks li
Are there remaining uses (or users) of the old document_dump /
document_dump_mode options? This corresponds to former options -D and -C
of isabelle usedir.
The meaning of these features has become quite difficult to define, so it
looks like they are better discontinued.
If there are remaini
13 matches
Mail list logo
