doc-src/Tutorial/Misc/arith2.ML
changeset 7840 e1fd12b864a1
parent 6577 a2b5c84d590a
equal deleted inserted replaced
7839:03fd460cb8b8 7840:e1fd12b864a1