[discarded1023]

The author, Larry Paulson, may or may not like ZF but he has a ton of experience in doing formal proofs in it.

https://isabelle.in.tum.de/website-Isabelle2020/dist/library...

[hackandthink]

Thanks, did not know.

Maybe this is the reason for his dislike. Would like to hear more about Larry Paulson's experience.

(maybe it was no fun at all)