src/HOL/equalities.ML
changeset 9502 50ec59aff389
parent 9447 e5180c869772
child 9608 a50dcf0475ad