src/HOL/Matrix_LP/matrixlp.ML
changeset 79836 c69ae2b8987e
parent 69597 ff784d5a5bfb
equal deleted inserted replaced
79835:866d96915388 79836:c69ae2b8987e