[isabelle-dev] lists_Int_eq

[Makarius]

Just another fine point concerning the 'a set business in current 
Isabelle/7f6668317e24: when remaking doc-src/TutorialI there is a change 
in doc-src/TutorialI/Inductive/document/Advanced.tex due to lists_Int_eq.

Its name indicates set operations, but it is now more general:

   listsp (inf (%x. x : ?A) (%x. x : ?B)) =
   inf (%x. x : lists ?A) (%x. x : lists ?B)

The recent change 1898e61e89c4 (berghofe) might be related.  Stefan should 
know what he had in mind.


 	Makarius