src/HOL/ex/LexProd.ML
changeset 1072 0140ff702b23
parent 972 e61b058d58d2
child 1465 5d7a7e439cec