src/HOL/Library/RBT.thy
changeset 36500 620f899158d4
parent 36245 af5fe3a72087
child 37027 98bfff1d159d