src/ZF/Ordinal.thy
changeset 32920 ccfb774af58c
parent 24893 b8ef7afe3a6b
child 35762 af3ff2ba4c54
equal deleted inserted replaced
32919:37adfa07b54b 32920:ccfb774af58c