src/HOL/Prod.ML
changeset 9230 17ae63f82ad8
parent 9020 1056cbbaeb29
child 9345 2f5f6824f888
equal deleted inserted replaced
9229:a7c6ea7e57de 9230:17ae63f82ad8