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_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
