src/HOL/equalities.ML
changeset 8039 a901bafe4578
parent 8030 af8db1872960
child 8121 4a53041acb28