src/HOL/Data_Structures/Selection.thy
changeset 73424 2b657a70116c
parent 73123 b4066bad7f76
child 73526 a3cc9fa1295d