src/HOL/Library/Code_Integer.thy
changeset 25459 d1dce7d0731c
parent 24999 1dbe785ed529
child 25767 852bce03412a
equal deleted inserted replaced
25458:ba8f5e4fa336 25459:d1dce7d0731c