[isabelle] auto and safe with defined variables in locales



In the following example:
locale A =
  fixes X
  defines "X==[1::nat]"

lemma (in A) test: "[] ~= X"
  apply safe

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
the locale.
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 MHonArc.