src/HOL/Library/Code_Integer.thy
changeset 25898 d8f17d8cf9d4
parent 25767 852bce03412a
child 25919 8b1c0d434824
equal deleted inserted replaced
25897:e9d45709bece 25898:d8f17d8cf9d4