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 in.tum.de>:
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
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