src/HOL/Multivariate_Analysis/normarith.ML
changeset 58839 ccda99401bc8
parent 58635 010b610eb55d
child 59580 cbc38731d42f