src/HOL/Analysis/normarith.ML
changeset 69981 3dced198b9ec
parent 69597 ff784d5a5bfb