src/HOL/Integ/IntDef.ML
changeset 7786 cf9d07ad62af
parent 7428 80838c2af97b
child 8937 7328d7c8d201