src/HOL/BNF_Cardinal_Arithmetic.thy
changeset 76371 1ac2416e8432
parent 75625 0dd3ac5fdbaa
child 76951 293caf3dbecd