src/HOL/Matrix_LP/ComputeFloat.thy
changeset 55238 7ddb889e23bd
parent 54489 03ff4d1e6784
child 56255 968667bbb8d2