diff -r 46f59511b7bb -r d97fdabd9e2b src/HOL/SPARK/Manual/Reference.thy --- a/src/HOL/SPARK/Manual/Reference.thy Fri Sep 20 19:07:10 2024 +0200 +++ b/src/HOL/SPARK/Manual/Reference.thy Fri Sep 20 19:51:08 2024 +0200 @@ -9,7 +9,7 @@ by (simp flip: mask_eq_exp_minus_1 take_bit_eq_mask take_bit_eq_mod) syntax (my_constrain output) - "_constrain" :: "logic => type => logic" ("_ :: _" [4, 0] 3) + "_constrain" :: "logic => type => logic" (\_ :: _\ [4, 0] 3) (*>*) chapter \HOL-\SPARK{} Reference\