src/HOL/Import/HOL/num.imp
changeset 18851 9502ce541f01
parent 17188 a26a4fc323ed
child 37387 3581483cca6c