diff -r 46f59511b7bb -r d97fdabd9e2b src/HOL/SMT_Examples/Boogie.thy --- a/src/HOL/SMT_Examples/Boogie.thy Fri Sep 20 19:07:10 2024 +0200 +++ b/src/HOL/SMT_Examples/Boogie.thy Fri Sep 20 19:51:08 2024 +0200 @@ -38,8 +38,8 @@ \ axiomatization - boogie_div :: "int \ int \ int" (infixl "div'_b" 70) and - boogie_mod :: "int \ int \ int" (infixl "mod'_b" 70) + boogie_div :: "int \ int \ int" (infixl \div'_b\ 70) and + boogie_mod :: "int \ int \ int" (infixl \mod'_b\ 70)