src/HOL/Matrix_LP/FloatSparseMatrixBuilder.ML
Wed, 26 Nov 2014 20:05:34 +0100 wenzelm renamed "pairself" to "apply2", in accordance to @{apply 2};
Fri, 17 May 2013 13:46:18 +0200 wenzelm tuned signature;
less more (0) -2 tip