src/HOL/Matrix_LP/ComputeFloat.thy
changeset 62958 b41c1cb5e251
parent 62348 9a5f43dac883
child 63167 0909deb8059b