src/HOL/Matrix_LP/ComputeFloat.thy
Mon, 05 Feb 2018 08:30:19 +0100 immler added lemmas, avoid 'float_of 0'
less more (0) -10 -1 tip