src/HOL/Matrix/ComputeFloat.thy
changeset 44571 bd91b77c4cd6
parent 42676 8724f20bf69c
child 45495 c55a07526dbe