src/HOL/Matrix_LP/ComputeFloat.thy
changeset 59350 acba5d6fdb2f
parent 58889 5b7a9633cfa8
child 60017 b785d6d06430