use lifting/transfer formalization of RBT from Lift_RBT
(* Title: HOL/Quotient_Examples/Lift_RBT.thy Author: Lukas Bulwahn and Ondrej Kuncar*)header {* Lifting operations of RBT trees *}theory Lift_RBT imports Main "~~/src/HOL/Library/RBT_Impl"begin(* Moved to ~~/HOL/Library/RBT" *)end