Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] print_statement does not quote variables with ...


view this post on Zulip Email Gateway (Aug 22 2022 at 14:13):

From: Makarius <makarius@sketis.net>
Yes, I have changed that in
http://isabelle.in.tum.de/repos/isabelle/rev/5076725247fa

Note that the long form with fixes/assumes/shows has become a bit
old-fashioned, although there is nothing wrong with it apart from being
too long for short statements.

The new eigen-context notation "theorem B if A for x" often works
better, but there no print command for that yet. In fact, I would like
to make the "for x" form standard for almost all output, e.g. plain
'thm'. But that is a different story for a different release.

Makarius

view this post on Zulip Email Gateway (Aug 22 2022 at 14:18):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear list,

I occasionally (e.g., when I refactor my theories) use print_statement some_thm to get
long statement of a theorem printed such that I can copy-paste the fixes and assumes part
into a "context fixes ... assumes ... begin" block. Now, I noticed that when a variable
has the name is reserved in the current outer syntax (for example, a variable called
oracle), then there are no quotes around the fixed variable.

Here's an example:

lemma foo: "oracle = 0 ==> 0 = oracle" by simp
print_statement foo
(* output:
theorem foo:
fixes oracle :: "'a"
and x :: "'a"
assumes "oracle = x"
shows "x = oracle"
*)

Could print_statement be changed such that the output encloses the variable "oracle" in
quotes? I.e.:

theorem foo:
fixes "oracle" :: "'a"
and x :: "'a"
assumes "oracle = x"
shows "x = oracle"

Thanks,
Andreas


Last updated: Mar 28 2024 at 12:29 UTC