src/HOL/Multivariate_Analysis/normarith.ML
changeset 55126 9f9db4e6fabc
parent 54742 7a86358a3c0b
child 58635 010b610eb55d