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 toplevel
statement:

lemma
includes test
shows "test xs = []" and "test ys = []"
proof -
show "test xs = []" by simp
next -- "redundant"
show "test ys = []" by simp
qed
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.

Yet another alternative keeps the context and the statement separate:

  context includes test
  begin

    lemma shows ...

  end


	Makarius





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