src/HOL/Induct/Perm.thy
changeset 11046 b5f5942781a0
parent 9101 b643f4d7b9e9