src/HOL/Induct/Perm.ML
changeset 8876 f797816932d7
parent 8527 ce6ae118b6b2
child 9747 043098ba5098