Email Gateway (Aug 22 2022 at 14:13): 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
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: Nov 21 2024 at 12:39 UTC