--- a/src/HOL/Bali/AxSem.thy Sun Aug 25 20:54:20 2024 +0200
+++ b/src/HOL/Bali/AxSem.thy Sun Aug 25 21:10:01 2024 +0200
@@ -205,6 +205,8 @@
syntax
"_peek_res" :: "pttrn \<Rightarrow> 'a assn \<Rightarrow> 'a assn" ("\<lambda>_:. _" [0,3] 3)
+syntax_consts
+ "_peek_res" == peek_res
translations
"\<lambda>w:. P" == "CONST peek_res (\<lambda>w. P)"
@@ -266,6 +268,8 @@
syntax
"_peek_st" :: "pttrn \<Rightarrow> 'a assn \<Rightarrow> 'a assn" ("\<lambda>_.. _" [0,3] 3)
+syntax_consts
+ "_peek_st" == peek_st
translations
"\<lambda>s.. P" == "CONST peek_st (\<lambda>s. P)"