src/HOL/Library/RBT_Set.thy
changeset 64877 31e9920a0dc1
parent 64272 f76b6dda2e56
child 66148 5e60c2d0a1f1
equal deleted inserted replaced
64876:65a247444100 64877:31e9920a0dc1