src/HOL/Import/shuffler.ML
changeset 20564 6857bd9f1a79
parent 20326 cbf31171c147
child 20854 f9cf9e62d11c
equal deleted inserted replaced
20563:44eda2314aab 20564:6857bd9f1a79