src/HOL/Matrix/ComputeFloat.thy
changeset 42986 11fd8c04ea24
parent 42676 8724f20bf69c
child 45495 c55a07526dbe