src/HOL/Matrix_LP/ComputeFloat.thy
changeset 82282 919eb0e67930
parent 69605 a96320074298