Email Gateway (Aug 19 2022 at 10:03): Email Gateway (Aug 19 2022 at 10:03):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Christian,
I guess the reason is that »d« does not depend on any parameter. Did
not go into possible technical reasons or the question whether this is
»well-behaved«.
Cheers,
Florian
signature.asc
Email Gateway (Aug 19 2022 at 10:24):From: Christian Sternagel <c.sternagel@gmail.com>
Dear all,
Consider the following (I used Isabelle2013-RC2, but the same thing
happens also with Isabelle2012):
locale test =
fixes c :: bool
begin
abbreviation "c' == c"
term c
definition "d = True"
abbreviation "d' == d"
term d
definition "e = c"
abbreviation "e' == e"
term e
end
for the output of "term c" the abbreviation is used, for "term d" not,
but again for "term e". Is this intended behavior?
Originally I noticed this kind of thing in
locale finite_tree =
fixes mk :: "'b ⇒ 'a list ⇒ 'a"
...
begin
...
inductive
subtree :: "'a ⇒ 'a ⇒ bool"
where
base [intro]: "t ∈ set ts ⟹ subtree t (mk x ts)" |
step [intro]: "subtree s t ⟹ t ∈ set ts ⟹ subtree s (mk x ts)"
abbreviation "subtreeeq == subtree^=="
term subtreeeq
...
end
where the abbreviation subtreeeq is also not used (but I wanted to have
such an abbreviation during document preparation).
cheers
chris
Last updated: Oct 30 2025 at 20:23 UTC