src/HOL/Num.thy
changeset 71208 5e0050eb64f2
parent 70927 cc204e10385c
child 71452 9edb7fb69bc2