src/HOL/Library/Code_Target_Numeral.thy
changeset 72278 199dc903131b
parent 60868 dd18c33c001e
equal deleted inserted replaced
72277:48254fa33d88 72278:199dc903131b