diff -r 46f59511b7bb -r d97fdabd9e2b src/HOL/Hoare/Hoare_Logic.thy --- a/src/HOL/Hoare/Hoare_Logic.thy Fri Sep 20 19:07:10 2024 +0200 +++ b/src/HOL/Hoare/Hoare_Logic.thy Fri Sep 20 19:51:08 2024 +0200 @@ -27,7 +27,7 @@ | Cond "'a bexp" "'a com" "'a com" | While "'a bexp" "'a com" -abbreviation annskip ("SKIP") where "SKIP == Basic id" +abbreviation annskip (\SKIP\) where "SKIP == Basic id" type_synonym 'a sem = "'a => 'a => bool"