Re: [isabelle] includes bundle works only in first case
On Wed, 30 May 2012, Andreas Lochbihler wrote:
Here is an alternative form that includes a bundle in the context of a
I read about that alternative, but I actually prefer "including" over
"includes", because including does not clutter the statement of the lemma
with hints to the prover.
shows "test xs = " and "test ys = "
show "test xs = " by simp
next -- "redundant"
show "test ys = " by simp
Yet another alternative keeps the context and the statement separate:
context includes test
lemma shows ...
This archive was generated by a fusion of
Pipermail (Mailman edition) and