src/HOL/Integ/Bin.ML
changeset 3450 cd73bc206d87
parent 2988 d38f330e58b3
child 3919 c036caebfc75
equal deleted inserted replaced
3449:6b17f82bbf01 3450:cd73bc206d87