src/HOL/Library/Set_Idioms.thy
changeset 70245 8feae28e5c44
parent 69918 eddcc7c726f3
child 77935 7f240b0dabd9