src/HOL/Quot/PER.thy
changeset 5253 82a5ca6290aa
parent 4531 20a7fddb706a