Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fixed csdp output parser
authorPhilipp Meyer
Thu, 26 Nov 2009 20:07:02 +0100
changeset 33906 1eebf19b773e
parent 33905 5760ba045bf0
child 33907 473f859e1c29
fixed csdp output parser
src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Thu Nov 26 15:28:42 2009 +0100
+++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Thu Nov 26 20:07:02 2009 +0100
@@ -537,8 +537,8 @@
  fun token s =
   Scan.repeat ($$ " ") |-- word s --| Scan.repeat ($$ " ")
  val numeral = Scan.one isnum
- val decimalint = Scan.repeat numeral >> (rat_of_string o implode)
- val decimalfrac = Scan.repeat numeral
+ val decimalint = Scan.repeat1 numeral >> (rat_of_string o implode)
+ val decimalfrac = Scan.repeat1 numeral
     >> (fn s => rat_of_string(implode s) // pow10 (length s))
  val decimalsig =
     decimalint -- Scan.option (Scan.$$ "." |-- decimalfrac)
isabelle