src/HOL/Quotient.thy
changeset 35366 6d474096698c
parent 35294 0e1adc24722f
child 35827 f552152d7747