src/HOL/Multivariate_Analysis/normarith.ML
changeset 51000 c9adb50f74ad
parent 48112 b1240319ef15
child 51717 9e7d1c139569