src/HOL/Multivariate_Analysis/normarith.ML
changeset 38968 e55deaa22fff
parent 37744 3daaf23b9ab4
child 39032 548e933b90ad