src/HOL/Product_Type.ML
changeset 14359 3d9948163018
parent 11838 02d75712061d