src/HOL/Code_Numeral.thy
changeset 61685 2b3772ecfdec
parent 61275 053ec04ea866
child 61857 542f2c6da692
equal deleted inserted replaced
61684:048ba34613bb 61685:2b3772ecfdec