src/HOL/Num.thy
changeset 55101 57c875e488bd
parent 54489 03ff4d1e6784
child 55415 05f5fdb8d093