src/HOL/Induct/Perm.thy
changeset 9356 30c3d3e308ee
parent 9101 b643f4d7b9e9