[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)
show "y∨x" using x_true by auto
However, when trying to prove a similar lemma, I don't know how to unfold
lemma (in dummy) "dummy.f True"
Any help is highly appreciated.
This archive was generated by a fusion of
Pipermail (Mailman edition) and