src/HOL/Set.ML
changeset 7887 eedfff88ee40
parent 7717 e7ecfa617443
child 7969 7a20317850ab