[isabelle] abbreviations in locales are not used for printing terms



Dear Isabelle users,

some abbreviations introduced in locales do not appear when terms or theorems using them are printed in the same context or in a class which is a sublocale. Is there an explanation for this behaviour?

In the following example, I would have expected "ab" in the output for the term and lemma commands in the locale and "s.ab" in the first two outputs for s.ab and s.lem in the class (print_abbrevs contains s.ab after the sublocale command). As expected, "cd" appears in the last two outputs for s.ab and s.lem, though I am not sure why it works now. The behaviour is similar if {True} is replaced with True (or with more complex expressions involving locale parameters, from which this example is abstracted).

theory A
imports Main
begin

locale l begin
abbreviation "ab ≡ {True}"
term ab (* output: "{True}" :: "bool set" *)
lemma lem: "ab = ab" .. (* output: theorem {True} = {True} *)
end

class c begin
sublocale s: l .
term s.ab (* output: "{True}" :: "bool set" *)
thm s.lem (* output: {True} = {True} *)

abbreviation "cd ≡ {True}"
term s.ab (* output: "cd" :: "bool set" *)
thm s.lem (* output: cd = cd *)
end

end

Any insights or workarounds to get ab/s.ab to print would be appreciated.

Cheers,
Walter





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