src/HOL/Matrix_LP/ComputeFloat.thy
changeset 64406 492de9062cd2
parent 63901 4ce989e962e0
child 65583 8d53b3bebab4
equal deleted inserted replaced
64405:81bac77929d9 64406:492de9062cd2