src/HOL/BNF_Cardinal_Arithmetic.thy
changeset 58831 aa8cf5eed06e
parent 56191 159b0c88b4a4
child 58889 5b7a9633cfa8