src/HOL/ex/LexProd.thy
changeset 1893 fa58f4a06f21
parent 1476 608483c2122a