src/HOL/Matrix/Compute_Oracle/compute.ML
changeset 38526 a9ce311eb6b9
parent 37872 d83659570337
child 38808 89ae86205739