src/HOL/Data_Structures/Selection.thy
changeset 73255 7e2a9a8c2b85
parent 73123 b4066bad7f76
child 73526 a3cc9fa1295d