src/HOL/Matrix/ComputeFloat.thy
changeset 41648 6d736d983d5c
parent 41550 efa734d9b221
child 41959 b460124855b8