[isabelle] Input/Output syntax for locale interpretation



Hi all,

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


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


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.

Regards,
  Peter





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