--- a/src/HOL/HOL.thy Sat Dec 14 23:48:45 2024 +0100
+++ b/src/HOL/HOL.thy Sun Dec 15 14:59:57 2024 +0100
@@ -233,6 +233,10 @@
where "Let s f \<equiv> f s"
nonterminal letbinds and letbind
+
+open_bundle let_syntax
+begin
+
syntax
"_bind" :: "[pttrn, 'a] \<Rightarrow> letbind" (\<open>(\<open>indent=2 notation=\<open>mixfix let binding\<close>\<close>_ =/ _)\<close> 10)
"" :: "letbind \<Rightarrow> letbinds" (\<open>_\<close>)
@@ -244,6 +248,8 @@
"_Let (_binds b bs) e" \<rightleftharpoons> "_Let b (_Let bs e)"
"let x = a in e" \<rightleftharpoons> "CONST Let a (\<lambda>x. e)"
+end
+
axiomatization undefined :: 'a
class default = fixes default :: 'a