src/HOL/Num.thy
changeset 71185 8a0e25d93a95
parent 70927 cc204e10385c
child 71452 9edb7fb69bc2