[isabelle-dev] lists_Int_eq

Makarius makarius at sketis.net
Thu Jan 12 16:06:27 CET 2012

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

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


More information about the isabelle-dev mailing list