src/HOL/Matrix_LP/ComputeFloat.thy
changeset 51796 f0ee854aa2bd
parent 48891 c0eafbd55de3
child 54489 03ff4d1e6784