src/HOL/Matrix_LP/ComputeFloat.thy
changeset 59894 ca16b657901f
parent 58889 5b7a9633cfa8
child 60017 b785d6d06430
equal deleted inserted replaced
59893:89f3bd11fa8b 59894:ca16b657901f