src/Pure/General/integer.ML
changeset 70845 8e51ea8d4609
parent 69729 4591221824f6
child 73019 05e2cab9af8b