-->
 <span style="color: #000000;">x</span><span style="color: #008000;">"1 2 34 5678_AbC"</span> <span style="color: #000080;font-style:italic;">-- same as {0x01, 0x02, 0x34, 0x56, 0x78, 0xAB, 0x0C}
                    -- note however it displays as {1,2,52,86,120,171,12}
                    -- whereas x"414243" displays as "ABC" (as all chars)</span>
<!--