[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

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

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 *)


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


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