src/HOL/Integ/Bin.ML
changeset 11295 66925f23ac7f
parent 10701 16493f0cee9a
child 11655 923e4d0d36d5