src/HOL/Code_Numeral.thy
changeset 81027 a9dc66e05297
parent 80088 5afbf04418ec
child 81639 7fa796a773a5
equal deleted inserted replaced
81026:c4bc259393f6 81027:a9dc66e05297