src/HOL/Data_Structures/Selection.thy
changeset 73616 b0ea03e837b1
parent 73526 a3cc9fa1295d
child 75501 426afab39a55