src/HOL/equalities.ML
changeset 3044 3e3087aa69e7
parent 2922 580647a879cf
child 3222 726a9b069947