src/HOL/Prod.ML
changeset 5242 3087dafb70ec
parent 5144 7ac22e5a05d7
child 5278 a903b66822e2