src/HOL/Num.thy
changeset 62979 1e527c40ae40
parent 62597 b3f2b8c906a6
child 63654 f90e3926e627