[isabelle-dev] lists_Int_eq

[Makarius]

On Wed, 11 Jan 2012, Stefan Berghofer wrote:

> If you look at the version of the tutorial available on the Isabelle
> web page (p. 141)
>
>  http://isabelle.in.tum.de/dist/Isabelle2011-1/doc/tutorial.pdf
>
> you will see that it has already been broken for some time, the only 
> difference being that set union is now printed as "inf", due to the 
> recent re-introduction of the set type.

Checking this in current Isabelle/55a4769d0abe the sentence in the 
tutorial now makes sense again:

   The subgoal may look uninviting, but fortunately lists distributes over
   intersection:

   lists (A ∩ B) = lists A ∩ lists B	(lists_Int_e


 	Makarius