src/HOL/Multivariate_Analysis/normarith.ML
changeset 59527 edaabc1ab1ed
parent 58635 010b610eb55d
child 59580 cbc38731d42f