[isabelle-dev] The-operator

Lars Noschinski noschinl at in.tum.de
Wed May 22 17:38:09 CEST 2013

On 22.05.2013 17:14, Roger H. wrote:
> how can i prove the following:
> ( THE A. {a. f a = {c1, c2, c3}} = {a. f a = A} ) = {c1, c2, c3} ?

This is a topic for the isabelle-users mailing list; this mailing list 
is for topics specific to the developer version of Isabelle.

But the answer is: You don't; nitpick will give you a counter-example.

   -- Lars

More information about the isabelle-dev mailing list