src/HOL/Num.thy
changeset 59520 76d7c593c6e8
parent 58889 5b7a9633cfa8
child 59621 291934bac95e