src/HOL/Matrix_LP/ComputeHOL.thy
changeset 59857 49b975c5f58d
parent 59582 0fbed69ff081
child 63167 0909deb8059b
equal deleted inserted replaced
59855:ffd50fdfc7fa 59857:49b975c5f58d