src/HOL/Code_Numeral.thy
changeset 77890 26d49c15bff0
parent 76053 3310317cc484
child 78669 18ea58bdcf77
equal deleted inserted replaced
77889:5db014c36f42 77890:26d49c15bff0