src/HOL/Code_Numeral.thy
changeset 79714 80cb54976c1c
parent 79673 c172eecba85d
child 80088 5afbf04418ec