src/HOL/Matrix_LP/float_arith.ML
changeset 80501 83c212f7cf97
parent 73019 05e2cab9af8b
equal deleted inserted replaced
80500:12dc23fc3135 80501:83c212f7cf97