| changeset 80914 | d97fdabd9e2b |
| parent 74723 | f05c73bf5968 |
| child 81191 | 60f46822a22c |
--- 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 (\<open>SKIP\<close>) where "SKIP == Basic id" type_synonym 'a sem = "'a => 'a => bool"