Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] ML/Isabelle Flags

view this post on Zulip Email Gateway (Aug 18 2022 at 19:05):

From: Not Sure <kuerzn@googlemail.com>
Hi!
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ü)?

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"

  1. Where could I have read this information?

Thanks

view this post on Zulip Email Gateway (Aug 18 2022 at 19:05):

From: Lars Noschinski <noschinl@in.tum.de>
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

Last updated: Nov 21 2024 at 12:39 UTC