src/HOL/Matrix/ComputeFloat.thy
changeset 46060 f94b7179a75d
parent 45495 c55a07526dbe