src/HOL/Algebra/SndIsomorphismGrp.thy
changeset 79527 f1f08ca40d96
parent 77406 c2013f617a70
child 81438 95c9af7483b1