src/HOL/equalities.ML
changeset 5330 8c9fadda81f4
parent 5319 7356d0c88b1b
child 5331 3d27b96a08b0