src/HOL/Code_Numeral.thy
changeset 67872 39b27d38a54c
parent 67399 eab6ce8368fa
child 67905 fe0f4eeceeb7