src/HOL/Arith.thy
changeset 9450 c97dba47e504
parent 9436 62bb04ab4b01
child 9618 ff8238561394