# [isabelle] A tricky problem with Isabelle locales

Dear Isabelle pros,

`I have encountered a tricky problem with Isabelle locales. Is there anyone
``kind enough to help?
`
Suppose we have a dummy locale and a definition:
locale dummy = fixes x::bool assumes x_true:x
definition (in dummy) f::bool where "f ≡ ∀y::bool. y∨x"
We can show the following lemma by unfolding 'f' first:
lemma (in dummy) f
proof (unfold f_def,rule)

` fix y
`` show "y∨x" using x_true by auto
` qed

`However, when trying to prove a similar lemma, I don't know how to unfold
``'f' :(
` lemma (in dummy) "dummy.f True"
Any help is highly appreciated.
Best regards,
Wenda Li

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