Re: [isabelle] Input/Output syntax for locale interpretation

You should be able to either introduce explicit abbreviations for your constants in the global theory, or, if suitable concepts are already available there, you might prefer to provide explicit mappings by adding "where" clauses to your interpretation.


Quoting Peter Lammich <lammich at>:

Hi all,

I have some locale that fixes quite a few parameters, as for example:

locale foo =
  fixes a b c :: nat
  definition "const1 == a<c"
  definition "const2 == a<c+b"

Now I want to interpret the locale, using some quite long
instantiations, eg:

interpretation prefix?: foo "(1+3)*7" "(1+9)*42" "91 - 11*2" .

All is nice up to here. However, when I start using the locale, e.g. in

lemma "const1 ==> const2"

then some horrible output occurs, that nobody want's to read any more:

foo.const1 ((1 + 3) * 7) (91 - 11 * 2) ==>
    foo.const2 ((1 + 3) * 7) ((1 + 9) * 42) (91 - 11 * 2)

How can I change this behaviour, such that I get the plain names in the
output (or, if I used prefix!, the prefixed names).
Note: The locale tutorial sais that the current behaviour is the
intended one, but does not mention how
to change it.


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