src/HOL/Matrix/ComputeHOL.thy
changeset 45135 5ba2f065c6f7
parent 38273 d31a34569542
child 46984 0f1e85fcf5f4