src/HOL/Algebra/Bij.thy
changeset 33572 d78f347515e0
parent 33057 764547b68538
child 35416 d8d7d1b785af