src/HOL/Code_Numeral.thy
changeset 44246 380a4677c55d
parent 39818 ff9e9d5ac171
child 44821 a92f65e174cf
equal deleted inserted replaced
44245:45fb4b29c267 44246:380a4677c55d