src/HOL/Matrix_LP/ComputeFloat.thy
changeset 61545 57000ac6291f
parent 60017 b785d6d06430
child 61609 77b453bd616f