src/HOL/subset.ML
changeset 4072 d0d32dd77440
parent 2893 2ee005e46d6d
child 4159 4aff9b7e5597
equal deleted inserted replaced
4071:4747aefbbc52 4072:d0d32dd77440