src/HOL/Matrix_LP/Compute_Oracle/compute.ML
changeset 69798 f610115ca3d0
parent 69597 ff784d5a5bfb
child 77730 4a174bea55e2
equal deleted inserted replaced
69797:7e5a7a11d5d1 69798:f610115ca3d0