src/ZF/OrderType.thy
changeset 58924 b48bbd380d59
parent 58871 c399ae4b836f
child 60770 240563fbf41d
equal deleted inserted replaced
58923:cb9b69cca999 58924:b48bbd380d59