[isabelle-dev] The-operator

[Lars Noschinski]

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