src/HOL/ex/Arith_Examples.thy
changeset 27017 1e0e8c1adf8c
parent 24328 83afe527504d
child 30686 47a32dd1b86e