src/HOL/Library/Target_Numeral.thy
changeset 49890 89eff795f757
parent 49834 b27bbb021df1