src/HOL/equalities.ML
changeset 4950 226f2cde9f4d
parent 4882 379314255a04
child 5069 3ea049f7979d