--- a/src/FOL/IFOL.thy Sun Aug 25 15:02:19 2024 +0200
+++ b/src/FOL/IFOL.thy Sun Aug 25 15:07:22 2024 +0200
@@ -102,8 +102,8 @@
where \<open>x \<noteq> y \<equiv> \<not> (x = y)\<close>
syntax "_Uniq" :: "pttrn \<Rightarrow> o \<Rightarrow> o" ("(2\<exists>\<^sub>\<le>\<^sub>1 _./ _)" [0, 10] 10)
+syntax_consts "_Uniq" \<rightleftharpoons> Uniq
translations "\<exists>\<^sub>\<le>\<^sub>1x. P" \<rightleftharpoons> "CONST Uniq (\<lambda>x. P)"
-syntax_consts "_Uniq" \<rightleftharpoons> Uniq
print_translation \<open>
[Syntax_Trans.preserve_binder_abs_tr' \<^const_syntax>\<open>Uniq\<close> \<^syntax_const>\<open>_Uniq\<close>]
@@ -747,10 +747,10 @@
"" :: \<open>letbind => letbinds\<close> (\<open>_\<close>)
"_binds" :: \<open>[letbind, letbinds] => letbinds\<close> (\<open>_;/ _\<close>)
"_Let" :: \<open>[letbinds, 'a] => 'a\<close> (\<open>(let (_)/ in (_))\<close> 10)
+syntax_consts "_Let" \<rightleftharpoons> Let
translations
"_Let(_binds(b, bs), e)" == "_Let(b, _Let(bs, e))"
"let x = a in e" == "CONST Let(a, \<lambda>x. e)"
-syntax_consts "_Let" \<rightleftharpoons> Let
lemma LetI:
assumes \<open>\<And>x. x = t \<Longrightarrow> P(u(x))\<close>