src/HOL/Code_Numeral.thy
changeset 80828 389e1bf96e05
parent 80088 5afbf04418ec
child 81639 7fa796a773a5
equal deleted inserted replaced
80827:2ef32d34ef1c 80828:389e1bf96e05