doc-src/Tutorial/Misc/arith2.ML
changeset 7858 2cd88d1eec0c
parent 6577 a2b5c84d590a
equal deleted inserted replaced
7857:a49a3978fe3a 7858:2cd88d1eec0c