src/HOL/Matrix_LP/ComputeFloat.thy
changeset 55989 55827fc7c0dd
parent 54489 03ff4d1e6784
child 56255 968667bbb8d2