Re: [isabelle] Domain proof

On Fr, 2014-01-17 at 18:03 +0200, Roger H. wrote:
> Hi,
> how can i prove
> lemma "dom (SOME b. dom b = A) = A"

You have to show that there is such a beast b, ie,

proof -
  obtain b where "dom b = A" ...
  thus ?thesis 
	sledgehammer (*Should find a proof now, using the rules for SOME,
probably SomeI*)

-- Peter

> Thank you!

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