src/HOL/Multivariate_Analysis/normarith.ML
changeset 63220 06cbfbaf39c5
parent 63211 0bec0d1d9998