--- a/src/HOL/Bali/Basis.thy Sun Aug 25 20:54:20 2024 +0200
+++ b/src/HOL/Bali/Basis.thy Sun Aug 25 21:10:01 2024 +0200
@@ -195,6 +195,10 @@
"_Oall" :: "[pttrn, 'a option, bool] \<Rightarrow> bool" ("(3\<forall>_\<in>_:/ _)" [0,0,10] 10)
"_Oex" :: "[pttrn, 'a option, bool] \<Rightarrow> bool" ("(3\<exists>_\<in>_:/ _)" [0,0,10] 10)
+syntax_consts
+ "_Oall" \<rightleftharpoons> Ball and
+ "_Oex" \<rightleftharpoons> Bex
+
translations
"\<forall>x\<in>A: P" \<rightleftharpoons> "\<forall>x\<in>CONST set_option A. P"
"\<exists>x\<in>A: P" \<rightleftharpoons> "\<exists>x\<in>CONST set_option A. P"
@@ -257,6 +261,8 @@
text \<open>list patterns -- extends pre-defined type "pttrn" used in abstractions\<close>
syntax
"_lpttrn" :: "[pttrn, pttrn] \<Rightarrow> pttrn" ("_#/_" [901,900] 900)
+syntax_consts
+ "_lpttrn" \<rightleftharpoons> lsplit
translations
"\<lambda>y # x # xs. b" \<rightleftharpoons> "CONST lsplit (\<lambda>y x # xs. b)"
"\<lambda>x # xs. b" \<rightleftharpoons> "CONST lsplit (\<lambda>x xs. b)"