Hi!
is_numeric() hat den Punkt als Dezimaltrennzeichen fest einkodiert.
Ich habe auch vergessen, wie die Einstellmöglichkeiten für Dezimalseparator und Tausender-Trenner in PHP heißen und ob PHP überhaupt diese Möglichkiet hat.
In der Syntax von PHP ist festgelegt, dass es nur den Punkt als Dezimalseparator gibt. Da gibt es nichts einzustellen, ansonsten würden Quelltexte nicht auf anderen Systemen laufen und man hätte diesbezüglich schon viele Problembeschreibungen lesen müssen.
Formatierungen zum Zwecke der Ausgabe stehen auf einem anderen Blatt. Und mir ist davon auch keine Umkehrfunktion in PHPs Lieferumfang bekannt.
Lo!