src/HOL/subset.ML
changeset 2920 feab36851df3
parent 2893 2ee005e46d6d
child 4159 4aff9b7e5597