src/HOL/Multivariate_Analysis/normarith.ML
changeset 58278 e89c7ac4ce16
parent 54742 7a86358a3c0b
child 58635 010b610eb55d
equal deleted inserted replaced
58277:0dcd3a623a6e 58278:e89c7ac4ce16