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