src/HOL/Data_Structures/Selection.thy
changeset 73975 8d93f9ca6518
parent 73526 a3cc9fa1295d
child 75501 426afab39a55