src/HOL/Code_Numeral.thy
changeset 60614 e39e6881985c
parent 60562 24af00b010cf
child 60758 d8d85a8172b5