src/HOL/Prod.ML
changeset 2919 953a47dc0519
parent 2886 fd5645efa43d
child 2935 998cb95fdd43