src/HOL/Multivariate_Analysis/normarith.ML
changeset 42518 57367832b81a
parent 42361 23f352990944
child 42793 88bee9f6eec7