src/HOL/Prod.ML
changeset 5526 e7617b57a3e6
parent 5361 1c6f72351075
child 5553 ae42b36a50c2