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