src/HOL/Multivariate_Analysis/normarith.ML
changeset 58916 229765cc3414
parent 58635 010b610eb55d
child 59580 cbc38731d42f