Email Gateway (Aug 18 2022 at 12:51): Email Gateway (Aug 18 2022 at 12:51):From: Holger Gast <gast@informatik.uni-tuebingen.de>
Dear Isabelle users,
I have just upgraded my (Ubuntu) emacs to 22.2.1
and see the following funny behaviour:
lemma "[| A; B |] ==> A"
yields:
goal (1 subgoal):
1. A ==> B ==> A
with ProofGeneral 3.7.1 (advertised as latest stable),
while starting the command line "isabelle -I" gives (correctly):
lemma "[| A; B |] ==> A";
proof (prove): step 0
goal (1 subgoal):
1. [| A; B |] ==> A
XSymbols and everything else seems to be working properly,
I also re-byte-compiled ProofGeneral.
Has any of you encountered a similar problem?
Thanks,
Holger
Email Gateway (Aug 18 2022 at 12:52):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Holger,
the printing of folded implications is controlled by the printmode; for
PG you can set it using the PROOFGENERAL_OPTIONS in your
~/.isabelle/etc/settings file. Can you check
isabelle getenv PROOFGENERAL_OPTIONS
If it contains "-m no_brackets", implications are not printed using
those funny brackets [| |]. If you really want them, adapt your
~/.isabelle/etc/settings accordingly and everything should be fine.
Hope this helps
Florian
signature.asc
Email Gateway (Aug 18 2022 at 12:52):From: Christian Sternagel <christian.sternagel@uibk.ac.at>
I think the standard behavior is to prefer [| A; B |] ==> A' over
A ==> B ==> A' for output. But I would not consider it a bug, if it is
done the other way round (since both formulas are logically equivalent).
I can't believe, however, that output behavior depends on the emacs
version. I think you just have a different Isabelle or ProofGeneral version.
cheers
christian
Holger Gast wrote:
Email Gateway (Aug 18 2022 at 12:52):From: Makarius <makarius@sketis.net>
As far as I know, the situation is still the same as it has been for more
than 10 years already. The system allows to write iterated arrows (both
=> on types, and ==> on props, i.e. "types of proofs") in
alternative bracket notation, e.g. like this:
'a => 'b => 'c vs. ['a, 'b] => 'c
A ==> B ==> C vs. [| A; B |] ==> C
Printing is controlled by print modes, with positive and negative modes to
allow explicit control independent of defaults coming from somewhere:
no_type_brackets type_brackets
no_brackets brackets
The default of the Isabelle distribution is no_type_brackets and brackets.
(Personally I always use no_type_brackets and no_brackets, both for
uniformity and for improved readability of nested rules; it also requires
less explanations to new users, assuming that "currying" is known
already.)
Makarius
Last updated: May 03 2024 at 08:18 UTC