src/HOL/Code_Numeral.thy
changeset 79517 0856026e2c88
parent 79489 1e19abf373ac
child 79531 22a137a6de44