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