src/HOL/Quotient_Examples/Lift_RBT.thy
changeset 47019 7bdac8e81f6d
parent 46133 d9fe85d3d2cd
child 47092 fa3538d6004b