src/HOL/Multivariate_Analysis/normarith.ML
changeset 60537 5398aa5a4df9
parent 59621 291934bac95e
child 60642 48dd1cefb4ae
equal deleted inserted replaced
60536:00db0d934a7d 60537:5398aa5a4df9