src/HOL/ex/LexProd.thy
changeset 1444 23ceb1dc9755
parent 1151 c820b3cc3df0
child 1476 608483c2122a