src/HOL/Multivariate_Analysis/normarith.ML
changeset 54260 6a967667fd45
parent 51717 9e7d1c139569
child 54742 7a86358a3c0b
equal deleted inserted replaced
54259:71c701dc5bf9 54260:6a967667fd45