src/HOL/Matrix/FloatArith.ML
changeset 15579 32bee18c675f
parent 15189 9cfbc392918c