src/HOL/Import/shuffler.ML
changeset 20864 bb75b876b260
parent 20854 f9cf9e62d11c
child 20897 3f8d2834b2c4
equal deleted inserted replaced
20863:4ee61dbf192d 20864:bb75b876b260