Re: [isabelle] ML/Isabelle Flags



On 07.02.2012 14:20, Not Sure wrote:
I am new to Isabelle (and ML) and have two questions:

1. Where do I enter the command

ML "set show_types"

in tty and ProofGeneral (not using the menü)?

The recommended way to enable the display of type information is

declare [[show_types]] (when you in a theory)

or

using [[show_types]] (when you are in a proof)

That being said, where did you get that command from? "set show_types" is not a valid ML fragment (at least in current Isabelle).

In tty I get this error:
*** Illegal application of command "ML" at top level
*** At command "ML"

in Proofgeneral this error:
*** Illegal application of command "ML" at top level
*** At command "ML"

Most commands are only valid when you are in a theory. Entering a theory ("theory Foo imports Main begin [...] end") is usually the first things you do in a theory file.

If you don't know Isabelle yet, the first part of the lecture notes at

  http://www4.in.tum.de/lehre/vorlesungen/semantik/WS1112/

should be a good start. There is also the Isabelle/Isar Reference Manual which tells you what exists, but not necessarily how to use it (without a certain amount of Isabelle knowledge).

  -- Lars





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