src/HOL/Num.thy
changeset 71418 bd9d27ccb3a3
parent 70927 cc204e10385c
child 71452 9edb7fb69bc2