src/HOL/Num.thy
changeset 71297 9f2085c499a2
parent 70927 cc204e10385c
child 71452 9edb7fb69bc2