src/HOL/Matrix_LP/ComputeFloat.thy
changeset 63103 2394b0db133f
parent 62348 9a5f43dac883
child 63167 0909deb8059b
equal deleted inserted replaced
63102:71059cf60658 63103:2394b0db133f