OK, my mistake, didn't read it sufficiently carefully.
It is not a double 5 V "buck" regulator but a 7-15 V to 5 V "buck" regulator together with a 7-15 V to 12 V "buck-boost" regulator. Still entirely suitable, albeit clearly overkill. 
Really a very useful device.