src/HOL/Finite.thy
changeset 11741 470e608d7a74
parent 11451 8abfb4f7bd02
child 11786 51ce34ef5113