[isabelle] auto and safe with defined variables in locales
In the following example:
locale A =
lemma (in A) test: " ~= X"
The subgoal presented to me is: False.
I expected something like:  = X ==> False, but I get just False.
The same is with auto. The reason seems to be the defined variable X of
In some more complex proofs, this forces me to very often fold/unfold
symbol definitions in my locales (to prevent auto or safe making such
transformations), and this makes the proof scripts more confusing.
Is this behaviour of safe and auto the intended one ?
Is there any workaround to use a defined variable like X, but prevent
safe/auto from making such steps ?
Thanks in advance for any help
-- Peter Lammich
This archive was generated by a fusion of
Pipermail (Mailman edition) and