src/HOL/Multivariate_Analysis/normarith.ML
changeset 52264 cdba0c3cb4c2
parent 51717 9e7d1c139569
child 54742 7a86358a3c0b