Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Library/Sum_of_Squares/sum_of_squares.ML
changeset 80910 406a85a25189
parent 74623 9b1d33c7bbcc 
--- a/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Fri Sep 20 13:30:55 2024 +0200
+++ b/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Fri Sep 20 14:28:13 2024 +0200
@@ -283,7 +283,7 @@
     val n = dim v
     val strs =
       map (decimalize 20 o (fn i => FuncUtil.Intfunc.tryapplyd (snd v) i @0)) (1 upto n)
-  in space_implode " " strs ^ "\n" end;
+  in implode_space strs ^ "\n" end;
 
 fun triple_int_ord ((a, b, c), (a', b', c')) =
   prod_ord int_ord (prod_ord int_ord int_ord) ((a, (b, c)), (a', (b', c')));
@@ -559,7 +559,7 @@
   in
     string_of_int m ^ "\n" ^
     string_of_int nblocks ^ "\n" ^
-    (space_implode " " (map string_of_int blocksizes)) ^
+    (implode_space (map string_of_int blocksizes)) ^
     "\n" ^
     sdpa_of_vector obj ^
     fold_rev (fn (k, m) => fn a => sdpa_of_blockdiagonal (k - 1) m ^ a)
isabelle