src/HOL/Num.thy
changeset 68724 7fafadbf16c7
parent 68536 e14848001c4c
child 69593 3dda49e08b9d