src/ZF/arith.ML
changeset 5951 e98c900540f9
parent 127 eec6bb9c58ea