src/HOL/Prod.ML
changeset 7982 d534b897ce39
parent 7958 f531589c9fc1
child 8100 6186ee807f2e
equal deleted inserted replaced
7981:5120a2a15d06 7982:d534b897ce39