src/HOL/Quotient.thy
changeset 47884 21c42b095c84
parent 47626 f7b1034cb9ce
child 48891 c0eafbd55de3