src/HOL/Tools/numeral_syntax.ML
changeset 9502 50ec59aff389
parent 9314 fd8b0f219879
child 10693 9e4a0e84d0d6
equal deleted inserted replaced
9501:9cd32060bbc8 9502:50ec59aff389