src/HOL/ex/Code_Nat_examples.thy
changeset 49177 db8ce685073f
parent 47108 2a1953f0d20d