src/Pure/General/integer.ML
changeset 72216 0d7cd97f6c48
parent 69729 4591221824f6
child 73019 05e2cab9af8b