src/HOL/Multivariate_Analysis/normarith.ML
changeset 63489 cd540c8031a4
parent 63211 0bec0d1d9998
equal deleted inserted replaced
63488:a7c5074a0251 63489:cd540c8031a4