src/HOL/Multivariate_Analysis/normarith.ML
changeset 57514 bdc2c6b40bf2
parent 54742 7a86358a3c0b
child 58635 010b610eb55d
equal deleted inserted replaced
57513:55b2afc5ddfc 57514:bdc2c6b40bf2