fixed csdp output parser
authorPhilipp Meyer
Thu Nov 26 20:07:02 2009 +0100 (2009-11-26)
changeset 339061eebf19b773e
parent 33905 5760ba045bf0
child 33907 473f859e1c29
fixed csdp output parser
src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML
     1.1 --- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Thu Nov 26 15:28:42 2009 +0100
     1.2 +++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Thu Nov 26 20:07:02 2009 +0100
     1.3 @@ -537,8 +537,8 @@
     1.4   fun token s =
     1.5    Scan.repeat ($$ " ") |-- word s --| Scan.repeat ($$ " ")
     1.6   val numeral = Scan.one isnum
     1.7 - val decimalint = Scan.repeat numeral >> (rat_of_string o implode)
     1.8 - val decimalfrac = Scan.repeat numeral
     1.9 + val decimalint = Scan.repeat1 numeral >> (rat_of_string o implode)
    1.10 + val decimalfrac = Scan.repeat1 numeral
    1.11      >> (fn s => rat_of_string(implode s) // pow10 (length s))
    1.12   val decimalsig =
    1.13      decimalint -- Scan.option (Scan.$$ "." |-- decimalfrac)