src/HOL/BNF_Cardinal_Arithmetic.thy
changeset 56846 9df717fef2bb
parent 56191 159b0c88b4a4
child 58889 5b7a9633cfa8