src/HOL/ex/LexProd.ML
changeset 1444 23ceb1dc9755
parent 972 e61b058d58d2
child 1465 5d7a7e439cec