src/HOL/Quotient.thy
changeset 45505 dc452a1a46e5
parent 44921 58eef4843641
child 45680 a61510361b89