src/HOL/Quotient_Examples/Lift_RBT.thy
changeset 45615 c05e8209a3aa
parent 45577 33b964e117bd
child 45629 ef08425dd2d5