src/HOL/Code_Numeral.thy
changeset 82595 c0587d661ea8
parent 82528 3704717ed7bf
child 82774 2865a6618cba