src/HOL/BNF_Wellorder_Embedding.thy
changeset 78176 41a2c9d5cd5d
parent 76950 f881fd264929
child 82248 e8c96013ea8a