src/HOL/Matrix/ComputeFloat.thy
changeset 36832 e6078ef937df
parent 35032 7efe662e41b4
child 38273 d31a34569542