[isabelle] abbreviations inside locales



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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.