src/HOL/Matrix_LP/ComputeFloat.thy
changeset 59927 251fa1530de1
parent 58889 5b7a9633cfa8
child 60017 b785d6d06430