src/HOL/Data_Structures/Selection.thy
changeset 73211 bfa9f646f5ae
parent 73123 b4066bad7f76
child 73526 a3cc9fa1295d