src/HOL/Matrix_LP/ComputeFloat.thy
changeset 65541 ae09b9f5980b
parent 63901 4ce989e962e0
child 65583 8d53b3bebab4