src/HOL/Code_Numeral.thy
changeset 82584 7ab0fb5d9919
parent 82528 3704717ed7bf
child 82774 2865a6618cba