src/HOL/Matrix_LP/ComputeFloat.thy
changeset 60243 5901cb4db0ae
parent 60017 b785d6d06430
child 61609 77b453bd616f