src/HOL/Matrix_LP/float_arith.ML
changeset 76522 3fc92362fbb5
parent 73019 05e2cab9af8b
equal deleted inserted replaced
76521:15f868460de9 76522:3fc92362fbb5