src/HOL/Num.thy
changeset 71751 abf3e80bd815
parent 71452 9edb7fb69bc2
child 71758 2e3fa4e7cd73