src/HOL/Num.thy
changeset 57998 8b7508f848ef
parent 57512 cc97b347b301
child 58112 8081087096ad