# HG changeset patch
# User wenzelm
# Date 1729258602 -7200
# Node ID c5b398584f5e5368e35f5357b5495ee601d51ebe
# Parent  f270cd6ee185f92f8146c7051fae3775ee721e54
tuned whitespace;

diff -r f270cd6ee185 -r c5b398584f5e src/HOL/Examples/Functions.thy
--- a/src/HOL/Examples/Functions.thy	Fri Oct 18 14:37:09 2024 +0200
+++ b/src/HOL/Examples/Functions.thy	Fri Oct 18 15:36:42 2024 +0200
@@ -333,7 +333,7 @@
     (if n \<le> 1 then Some [n]
      else if even n
        then do { ns \<leftarrow> collatz (n div 2); Some (n # ns) }
-       else do { ns \<leftarrow> collatz (3 * n + 1);  Some (n # ns)})"
+       else do { ns \<leftarrow> collatz (3 * n + 1); Some (n # ns)})"
 
 declare collatz.simps[code]
 value "collatz 23"