--- a/src/Benchmarks/Quickcheck_Benchmark/Needham_Schroeder_Base.thy Sun Aug 25 20:54:20 2024 +0200
+++ b/src/Benchmarks/Quickcheck_Benchmark/Needham_Schroeder_Base.thy Sun Aug 25 21:10:01 2024 +0200
@@ -28,6 +28,8 @@
syntax
"_MTuple" :: "['a, args] => 'a * 'b" ("(2\<lbrace>_,/ _\<rbrace>)")
+syntax_consts
+ "_MTuple" == MPair
translations
"\<lbrace>x, y, z\<rbrace>" == "\<lbrace>x, \<lbrace>y, z\<rbrace>\<rbrace>"
"\<lbrace>x, y\<rbrace>" == "CONST MPair x y"
--- a/src/Doc/Tutorial/Protocol/Message.thy Sun Aug 25 20:54:20 2024 +0200
+++ b/src/Doc/Tutorial/Protocol/Message.thy Sun Aug 25 21:10:01 2024 +0200
@@ -81,6 +81,8 @@
text\<open>Concrete syntax: messages appear as \<open>\<lbrace>A,B,NA\<rbrace>\<close>, etc...\<close>
syntax
"_MTuple" :: "['a, args] \<Rightarrow> 'a * 'b" ("(2\<lbrace>_,/ _\<rbrace>)")
+syntax_consts
+ "_MTuple" == MPair
translations
"\<lbrace>x, y, z\<rbrace>" == "\<lbrace>x, \<lbrace>y, z\<rbrace>\<rbrace>"
"\<lbrace>x, y\<rbrace>" == "CONST MPair x y"
--- a/src/HOL/Algebra/FiniteProduct.thy Sun Aug 25 20:54:20 2024 +0200
+++ b/src/HOL/Algebra/FiniteProduct.thy Sun Aug 25 21:10:01 2024 +0200
@@ -308,6 +308,8 @@
syntax
"_finprod" :: "index \<Rightarrow> idt \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"
("(3\<Otimes>__\<in>_. _)" [1000, 0, 51, 10] 10)
+syntax_consts
+ "_finprod" \<rightleftharpoons> finprod
translations
"\<Otimes>\<^bsub>G\<^esub>i\<in>A. b" \<rightleftharpoons> "CONST finprod G (%i. b) A"
\<comment> \<open>Beware of argument permutation!\<close>
--- a/src/HOL/Algebra/Lattice.thy Sun Aug 25 20:54:20 2024 +0200
+++ b/src/HOL/Algebra/Lattice.thy Sun Aug 25 21:10:01 2024 +0200
@@ -36,6 +36,10 @@
"_sup1" :: "('a, 'b) gorder_scheme \<Rightarrow> pttrns \<Rightarrow> 'a \<Rightarrow> 'a" ("(3SSUP\<index> _./ _)" [0, 10] 10)
"_sup" :: "('a, 'b) gorder_scheme \<Rightarrow> pttrn \<Rightarrow> 'c set \<Rightarrow> 'a \<Rightarrow> 'a" ("(3SSUP\<index> _:_./ _)" [0, 0, 10] 10)
+syntax_consts
+ "_inf1" "_inf" == infi and
+ "_sup1" "_sup" == supr
+
translations
"IINF\<^bsub>L\<^esub> x. B" == "CONST infi L CONST UNIV (%x. B)"
"IINF\<^bsub>L\<^esub> x:A. B" == "CONST infi L A (%x. B)"
--- a/src/HOL/Algebra/Ring.thy Sun Aug 25 20:54:20 2024 +0200
+++ b/src/HOL/Algebra/Ring.thy Sun Aug 25 21:10:01 2024 +0200
@@ -46,6 +46,8 @@
syntax
"_finsum" :: "index \<Rightarrow> idt \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"
("(3\<Oplus>__\<in>_. _)" [1000, 0, 51, 10] 10)
+syntax_consts
+ "_finsum" \<rightleftharpoons> finsum
translations
"\<Oplus>\<^bsub>G\<^esub>i\<in>A. b" \<rightleftharpoons> "CONST finsum G (\<lambda>i. b) A"
\<comment> \<open>Beware of argument permutation!\<close>
--- a/src/HOL/Analysis/Bochner_Integration.thy Sun Aug 25 20:54:20 2024 +0200
+++ b/src/HOL/Analysis/Bochner_Integration.thy Sun Aug 25 21:10:01 2024 +0200
@@ -892,12 +892,18 @@
syntax
"_lebesgue_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> 'a measure \<Rightarrow> real" ("\<integral>((2 _./ _)/ \<partial>_)" [60,61] 110)
+syntax_consts
+ "_lebesgue_integral" == lebesgue_integral
+
translations
"\<integral> x. f \<partial>M" == "CONST lebesgue_integral M (\<lambda>x. f)"
syntax
"_ascii_lebesgue_integral" :: "pttrn \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real" ("(3LINT (1_)/|(_)./ _)" [0,110,60] 60)
+syntax_consts
+ "_ascii_lebesgue_integral" == lebesgue_integral
+
translations
"LINT x|M. f" == "CONST lebesgue_integral M (\<lambda>x. f)"
--- a/src/HOL/Analysis/Euclidean_Space.thy Sun Aug 25 20:54:20 2024 +0200
+++ b/src/HOL/Analysis/Euclidean_Space.thy Sun Aug 25 21:10:01 2024 +0200
@@ -34,6 +34,7 @@
"(\<forall>u\<in>Basis. inner x u = 0) \<longleftrightarrow> (x = 0)"
syntax "_type_dimension" :: "type \<Rightarrow> nat" ("(1DIM/(1'(_')))")
+syntax_consts "_type_dimension" \<rightleftharpoons> card
translations "DIM('a)" \<rightharpoonup> "CONST card (CONST Basis :: 'a set)"
typed_print_translation \<open>
[(\<^const_syntax>\<open>card\<close>,
--- a/src/HOL/Analysis/Finite_Cartesian_Product.thy Sun Aug 25 20:54:20 2024 +0200
+++ b/src/HOL/Analysis/Finite_Cartesian_Product.thy Sun Aug 25 21:10:01 2024 +0200
@@ -40,6 +40,7 @@
\<^item> \<open>'a^'b::_\<close> becomes \<open>('a, 'b) vec\<close> without extra sort-constraint
\<close>
syntax "_vec_type" :: "type \<Rightarrow> type \<Rightarrow> type" (infixl "^" 15)
+syntax_types "_vec_type" \<rightleftharpoons> vec
parse_translation \<open>
let
fun vec t u = Syntax.const \<^type_syntax>\<open>vec\<close> $ t $ u;
--- a/src/HOL/Analysis/Finite_Product_Measure.thy Sun Aug 25 20:54:20 2024 +0200
+++ b/src/HOL/Analysis/Finite_Product_Measure.thy Sun Aug 25 21:10:01 2024 +0200
@@ -170,6 +170,8 @@
syntax
"_PiM" :: "pttrn \<Rightarrow> 'i set \<Rightarrow> 'a measure \<Rightarrow> ('i => 'a) measure" ("(3\<Pi>\<^sub>M _\<in>_./ _)" 10)
+syntax_consts
+ "_PiM" == PiM
translations
"\<Pi>\<^sub>M x\<in>I. M" == "CONST PiM I (%x. M)"
--- a/src/HOL/Analysis/Infinite_Set_Sum.thy Sun Aug 25 20:54:20 2024 +0200
+++ b/src/HOL/Analysis/Infinite_Set_Sum.thy Sun Aug 25 21:10:01 2024 +0200
@@ -100,6 +100,8 @@
syntax
"_infsetsum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::{banach, second_countable_topology}"
("(2\<Sum>\<^sub>a_\<in>_./ _)" [0, 51, 10] 10)
+syntax_consts
+ "_infsetsum" \<rightleftharpoons> infsetsum
translations \<comment> \<open>Beware of argument permutation!\<close>
"\<Sum>\<^sub>ai\<in>A. b" \<rightleftharpoons> "CONST infsetsum (\<lambda>i. b) A"
@@ -109,6 +111,8 @@
syntax
"_uinfsetsum" :: "pttrn \<Rightarrow> 'b \<Rightarrow> 'b::{banach, second_countable_topology}"
("(2\<Sum>\<^sub>a_./ _)" [0, 10] 10)
+syntax_consts
+ "_uinfsetsum" \<rightleftharpoons> infsetsum
translations \<comment> \<open>Beware of argument permutation!\<close>
"\<Sum>\<^sub>ai. b" \<rightleftharpoons> "CONST infsetsum (\<lambda>i. b) (CONST UNIV)"
@@ -118,6 +122,8 @@
syntax
"_qinfsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a::{banach, second_countable_topology}"
("(2\<Sum>\<^sub>a_ | (_)./ _)" [0, 0, 10] 10)
+syntax_consts
+ "_qinfsetsum" \<rightleftharpoons> infsetsum
translations
"\<Sum>\<^sub>ax|P. t" => "CONST infsetsum (\<lambda>x. t) {x. P}"
--- a/src/HOL/Analysis/Infinite_Sum.thy Sun Aug 25 20:54:20 2024 +0200
+++ b/src/HOL/Analysis/Infinite_Sum.thy Sun Aug 25 21:10:01 2024 +0200
@@ -50,6 +50,8 @@
"_infsum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::topological_comm_monoid_add" ("(3INFSUM (_/:_)./ _)" [0, 51, 10] 10)
syntax
"_infsum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::topological_comm_monoid_add" ("(2\<Sum>\<^sub>\<infinity>(_/\<in>_)./ _)" [0, 51, 10] 10)
+syntax_consts
+ "_infsum" \<rightleftharpoons> infsum
translations \<comment> \<open>Beware of argument permutation!\<close>
"\<Sum>\<^sub>\<infinity>i\<in>A. b" \<rightleftharpoons> "CONST infsum (\<lambda>i. b) A"
@@ -57,6 +59,8 @@
"_univinfsum" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a" ("(3INFSUM _./ _)" [0, 10] 10)
syntax
"_univinfsum" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a" ("(2\<Sum>\<^sub>\<infinity>_./ _)" [0, 10] 10)
+syntax_consts
+ "_univinfsum" \<rightleftharpoons> infsum
translations
"\<Sum>\<^sub>\<infinity>x. t" \<rightleftharpoons> "CONST infsum (\<lambda>x. t) (CONST UNIV)"
@@ -64,6 +68,8 @@
"_qinfsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3INFSUM _ |/ _./ _)" [0, 0, 10] 10)
syntax
"_qinfsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(2\<Sum>\<^sub>\<infinity>_ | (_)./ _)" [0, 0, 10] 10)
+syntax_consts
+ "_qinfsum" \<rightleftharpoons> infsum
translations
"\<Sum>\<^sub>\<infinity>x|P. t" => "CONST infsum (\<lambda>x. t) {x. P}"
--- a/src/HOL/Analysis/Interval_Integral.thy Sun Aug 25 20:54:20 2024 +0200
+++ b/src/HOL/Analysis/Interval_Integral.thy Sun Aug 25 21:10:01 2024 +0200
@@ -148,6 +148,9 @@
"_ascii_interval_lebesgue_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real measure \<Rightarrow> real \<Rightarrow> real"
("(5LINT _=_.._|_. _)" [0,60,60,61,100] 60)
+syntax_consts
+ "_ascii_interval_lebesgue_integral" == interval_lebesgue_integral
+
translations
"LINT x=a..b|M. f" == "CONST interval_lebesgue_integral M a b (\<lambda>x. f)"
@@ -159,6 +162,9 @@
"_ascii_interval_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real"
("(4LBINT _=_.._. _)" [0,60,60,61] 60)
+syntax_consts
+ "_ascii_interval_lebesgue_borel_integral" == interval_lebesgue_integral
+
translations
"LBINT x=a..b. f" == "CONST interval_lebesgue_integral CONST lborel a b (\<lambda>x. f)"
@@ -1045,11 +1051,17 @@
syntax "_complex_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> complex"
("(2CLBINT _. _)" [0,60] 60)
+syntax_consts
+ "_complex_lebesgue_borel_integral" == complex_lebesgue_integral
+
translations "CLBINT x. f" == "CONST complex_lebesgue_integral CONST lborel (\<lambda>x. f)"
syntax "_complex_set_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real set \<Rightarrow> real \<Rightarrow> complex"
("(3CLBINT _:_. _)" [0,60,61] 60)
+syntax_consts
+ "_complex_set_lebesgue_borel_integral" == complex_set_lebesgue_integral
+
translations
"CLBINT x:A. f" == "CONST complex_set_lebesgue_integral CONST lborel A (\<lambda>x. f)"
@@ -1065,6 +1077,9 @@
"_ascii_complex_interval_lebesgue_borel_integral" :: "pttrn \<Rightarrow> ereal \<Rightarrow> ereal \<Rightarrow> real \<Rightarrow> complex"
("(4CLBINT _=_.._. _)" [0,60,60,61] 60)
+syntax_consts
+ "_ascii_complex_interval_lebesgue_borel_integral" == complex_interval_lebesgue_integral
+
translations
"CLBINT x=a..b. f" == "CONST complex_interval_lebesgue_integral CONST lborel a b (\<lambda>x. f)"
--- a/src/HOL/Analysis/Measure_Space.thy Sun Aug 25 20:54:20 2024 +0200
+++ b/src/HOL/Analysis/Measure_Space.thy Sun Aug 25 21:10:01 2024 +0200
@@ -1006,6 +1006,9 @@
syntax
"_almost_everywhere" :: "pttrn \<Rightarrow> 'a \<Rightarrow> bool \<Rightarrow> bool" ("AE _ in _. _" [0,0,10] 10)
+syntax_consts
+ "_almost_everywhere" \<rightleftharpoons> almost_everywhere
+
translations
"AE x in M. P" \<rightleftharpoons> "CONST almost_everywhere M (\<lambda>x. P)"
@@ -1016,6 +1019,9 @@
"_set_almost_everywhere" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a \<Rightarrow> bool \<Rightarrow> bool"
("AE _\<in>_ in _./ _" [0,0,0,10] 10)
+syntax_consts
+ "_set_almost_everywhere" \<rightleftharpoons> set_almost_everywhere
+
translations
"AE x\<in>A in M. P" \<rightleftharpoons> "CONST set_almost_everywhere A M (\<lambda>x. P)"
--- a/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy Sun Aug 25 20:54:20 2024 +0200
+++ b/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy Sun Aug 25 21:10:01 2024 +0200
@@ -586,6 +586,9 @@
syntax
"_simple_integral" :: "pttrn \<Rightarrow> ennreal \<Rightarrow> 'a measure \<Rightarrow> ennreal" ("\<integral>\<^sup>S _. _ \<partial>_" [60,61] 110)
+syntax_consts
+ "_simple_integral" == simple_integral
+
translations
"\<integral>\<^sup>S x. f \<partial>M" == "CONST simple_integral M (%x. f)"
@@ -819,6 +822,9 @@
syntax
"_nn_integral" :: "pttrn \<Rightarrow> ennreal \<Rightarrow> 'a measure \<Rightarrow> ennreal" ("\<integral>\<^sup>+((2 _./ _)/ \<partial>_)" [60,61] 110)
+syntax_consts
+ "_nn_integral" == nn_integral
+
translations
"\<integral>\<^sup>+x. f \<partial>M" == "CONST nn_integral M (\<lambda>x. f)"
--- a/src/HOL/Analysis/Set_Integral.thy Sun Aug 25 20:54:20 2024 +0200
+++ b/src/HOL/Analysis/Set_Integral.thy Sun Aug 25 21:10:01 2024 +0200
@@ -26,6 +26,9 @@
"_ascii_set_lebesgue_integral" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real"
("(4LINT (_):(_)/|(_)./ _)" [0,0,0,10] 10)
+syntax_consts
+ "_ascii_set_lebesgue_integral" == set_lebesgue_integral
+
translations
"LINT x:A|M. f" == "CONST set_lebesgue_integral M A (\<lambda>x. f)"
@@ -576,6 +579,9 @@
"_complex_lebesgue_integral" :: "pttrn \<Rightarrow> complex \<Rightarrow> 'a measure \<Rightarrow> complex"
("\<integral>\<^sup>C _. _ \<partial>_" [0,0] 110)
+syntax_consts
+ "_complex_lebesgue_integral" == complex_lebesgue_integral
+
translations
"\<integral>\<^sup>Cx. f \<partial>M" == "CONST complex_lebesgue_integral M (\<lambda>x. f)"
@@ -583,6 +589,9 @@
"_ascii_complex_lebesgue_integral" :: "pttrn \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real"
("(3CLINT _|_. _)" [0,0,10] 10)
+syntax_consts
+ "_ascii_complex_lebesgue_integral" == complex_lebesgue_integral
+
translations
"CLINT x|M. f" == "CONST complex_lebesgue_integral M (\<lambda>x. f)"
@@ -617,6 +626,9 @@
"_ascii_complex_set_lebesgue_integral" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real"
("(4CLINT _:_|_. _)" [0,0,0,10] 10)
+syntax_consts
+ "_ascii_complex_set_lebesgue_integral" == complex_set_lebesgue_integral
+
translations
"CLINT x:A|M. f" == "CONST complex_set_lebesgue_integral M A (\<lambda>x. f)"
@@ -640,6 +652,10 @@
"_set_lebesgue_integral" :: "pttrn => 'a set => 'a measure => ereal => ereal"
("(\<integral>((_)\<in>(_)./ _)/\<partial>_)" [0,0,0,110] 10)
+syntax_consts
+"_set_nn_integral" == set_nn_integral and
+"_set_lebesgue_integral" == set_lebesgue_integral
+
translations
"\<integral>\<^sup>+x \<in> A. f \<partial>M" == "CONST set_nn_integral M A (\<lambda>x. f)"
"\<integral>x \<in> A. f \<partial>M" == "CONST set_lebesgue_integral M A (\<lambda>x. f)"
--- a/src/HOL/Analysis/Sparse_In.thy Sun Aug 25 20:54:20 2024 +0200
+++ b/src/HOL/Analysis/Sparse_In.thy Sun Aug 25 21:10:01 2024 +0200
@@ -166,11 +166,15 @@
syntax
"_eventually_cosparse" :: "pttrn => 'a set => bool => bool" ("(3\<forall>\<^sub>\<approx>_\<in>_./ _)" [0, 0, 10] 10)
+syntax_consts
+ "_eventually_cosparse" == eventually
translations
"\<forall>\<^sub>\<approx>x\<in>A. P" == "CONST eventually (\<lambda>x. P) (CONST cosparse A)"
syntax
"_qeventually_cosparse" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<forall>\<^sub>\<approx>_ | (_)./ _)" [0, 0, 10] 10)
+syntax_consts
+ "_qeventually_cosparse" == eventually
translations
"\<forall>\<^sub>\<approx>x|P. t" => "CONST eventually (\<lambda>x. t) (CONST cosparse {x. P})"
--- a/src/HOL/Auth/Message.thy Sun Aug 25 20:54:20 2024 +0200
+++ b/src/HOL/Auth/Message.thy Sun Aug 25 21:10:01 2024 +0200
@@ -51,6 +51,8 @@
text\<open>Concrete syntax: messages appear as \<open>\<lbrace>A,B,NA\<rbrace>\<close>, etc...\<close>
syntax
"_MTuple" :: "['a, args] \<Rightarrow> 'a * 'b" ("(2\<lbrace>_,/ _\<rbrace>)")
+syntax_consts
+ "_MTuple" \<rightleftharpoons> MPair
translations
"\<lbrace>x, y, z\<rbrace>" \<rightleftharpoons> "\<lbrace>x, \<lbrace>y, z\<rbrace>\<rbrace>"
"\<lbrace>x, y\<rbrace>" \<rightleftharpoons> "CONST MPair x y"
--- 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)"
--- 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)"
--- a/src/HOL/Bali/State.thy Sun Aug 25 20:54:20 2024 +0200
+++ b/src/HOL/Bali/State.thy Sun Aug 25 21:10:01 2024 +0200
@@ -135,6 +135,10 @@
Heap :: "loc \<Rightarrow> oref"
Stat :: "qtname \<Rightarrow> oref"
+syntax_consts
+ Heap == Inl and
+ Stat == Inr
+
translations
"Heap" => "CONST Inl"
"Stat" => "CONST Inr"
--- a/src/HOL/Codegenerator_Test/Code_Lazy_Test.thy Sun Aug 25 20:54:20 2024 +0200
+++ b/src/HOL/Codegenerator_Test/Code_Lazy_Test.thy Sun Aug 25 21:10:01 2024 +0200
@@ -24,6 +24,7 @@
no_notation lazy_llist ("_")
syntax "_llist" :: "args => 'a list" ("\<^bold>[(_)\<^bold>]")
+syntax_consts "_llist" == lazy_llist
translations
"\<^bold>[x, xs\<^bold>]" == "x\<^bold>#\<^bold>[xs\<^bold>]"
"\<^bold>[x\<^bold>]" == "x\<^bold>#\<^bold>[\<^bold>]"
--- a/src/HOL/HOLCF/Cfun.thy Sun Aug 25 20:54:20 2024 +0200
+++ b/src/HOL/HOLCF/Cfun.thy Sun Aug 25 21:10:01 2024 +0200
@@ -52,6 +52,9 @@
syntax
"_Lambda" :: "[cargs, logic] \<Rightarrow> logic" ("(3\<Lambda> _./ _)" [1000, 10] 10)
+syntax_consts
+ "_Lambda" \<rightleftharpoons> Abs_cfun
+
parse_ast_translation \<open>
(* rewrite (LAM x y z. t) => (_cabs x (_cabs y (_cabs z t))) *)
(* cf. Syntax.lambda_ast_tr from src/Pure/Syntax/syn_trans.ML *)
--- a/src/HOL/HOLCF/ConvexPD.thy Sun Aug 25 20:54:20 2024 +0200
+++ b/src/HOL/HOLCF/ConvexPD.thy Sun Aug 25 21:10:01 2024 +0200
@@ -181,6 +181,9 @@
syntax
"_convex_pd" :: "args \<Rightarrow> logic" ("{_}\<natural>")
+syntax_consts
+ "_convex_pd" == convex_add
+
translations
"{x,xs}\<natural>" == "{x}\<natural> \<union>\<natural> {xs}\<natural>"
"{x}\<natural>" == "CONST convex_unit\<cdot>x"
@@ -348,6 +351,9 @@
"_convex_bind" :: "[logic, logic, logic] \<Rightarrow> logic"
("(3\<Union>\<natural>_\<in>_./ _)" [0, 0, 10] 10)
+syntax_consts
+ "_convex_bind" == convex_bind
+
translations
"\<Union>\<natural>x\<in>xs. e" == "CONST convex_bind\<cdot>xs\<cdot>(\<Lambda> x. e)"
--- a/src/HOL/HOLCF/IOA/Sequence.thy Sun Aug 25 20:54:20 2024 +0200
+++ b/src/HOL/HOLCF/IOA/Sequence.thy Sun Aug 25 21:10:01 2024 +0200
@@ -72,6 +72,8 @@
syntax
"_totlist" :: "args \<Rightarrow> 'a Seq" ("[(_)!]")
"_partlist" :: "args \<Rightarrow> 'a Seq" ("[(_)?]")
+syntax_consts
+ "_totlist" "_partlist" \<rightleftharpoons> Consq
translations
"[x, xs!]" \<rightleftharpoons> "x \<leadsto> [xs!]"
"[x!]" \<rightleftharpoons> "x\<leadsto>nil"
--- a/src/HOL/HOLCF/LowerPD.thy Sun Aug 25 20:54:20 2024 +0200
+++ b/src/HOL/HOLCF/LowerPD.thy Sun Aug 25 21:10:01 2024 +0200
@@ -136,6 +136,9 @@
syntax
"_lower_pd" :: "args \<Rightarrow> logic" ("{_}\<flat>")
+syntax_consts
+ "_lower_pd" == lower_add
+
translations
"{x,xs}\<flat>" == "{x}\<flat> \<union>\<flat> {xs}\<flat>"
"{x}\<flat>" == "CONST lower_unit\<cdot>x"
@@ -342,6 +345,9 @@
"_lower_bind" :: "[logic, logic, logic] \<Rightarrow> logic"
("(3\<Union>\<flat>_\<in>_./ _)" [0, 0, 10] 10)
+syntax_consts
+ "_lower_bind" == lower_bind
+
translations
"\<Union>\<flat>x\<in>xs. e" == "CONST lower_bind\<cdot>xs\<cdot>(\<Lambda> x. e)"
--- a/src/HOL/HOLCF/Pcpo.thy Sun Aug 25 20:54:20 2024 +0200
+++ b/src/HOL/HOLCF/Pcpo.thy Sun Aug 25 21:10:01 2024 +0200
@@ -153,6 +153,7 @@
text \<open>Old "UU" syntax:\<close>
syntax UU :: logic
+syntax_consts UU \<rightleftharpoons> bottom
translations "UU" \<rightharpoonup> "CONST bottom"
text \<open>Simproc to rewrite \<^term>\<open>\<bottom> = x\<close> to \<^term>\<open>x = \<bottom>\<close>.\<close>
--- a/src/HOL/HOLCF/Porder.thy Sun Aug 25 20:54:20 2024 +0200
+++ b/src/HOL/HOLCF/Porder.thy Sun Aug 25 21:10:01 2024 +0200
@@ -118,6 +118,9 @@
syntax
"_BLub" :: "[pttrn, 'a set, 'b] \<Rightarrow> 'b" ("(3\<Squnion>_\<in>_./ _)" [0,0, 10] 10)
+syntax_consts
+ "_BLub" \<rightleftharpoons> lub
+
translations
"LUB x:A. t" \<rightleftharpoons> "CONST lub ((\<lambda>x. t) ` A)"
--- a/src/HOL/HOLCF/Representable.thy Sun Aug 25 20:54:20 2024 +0200
+++ b/src/HOL/HOLCF/Representable.thy Sun Aug 25 21:10:01 2024 +0200
@@ -32,6 +32,7 @@
assumes cast_liftdefl: "cast\<cdot>(liftdefl TYPE('a)) = liftemb oo liftprj"
syntax "_LIFTDEFL" :: "type \<Rightarrow> logic" ("(1LIFTDEFL/(1'(_')))")
+syntax_consts "_LIFTDEFL" \<rightleftharpoons> liftdefl
translations "LIFTDEFL('t)" \<rightleftharpoons> "CONST liftdefl TYPE('t)"
definition liftdefl_of :: "udom defl \<rightarrow> udom u defl"
@@ -51,6 +52,7 @@
assumes liftdefl_eq: "liftdefl TYPE('a) = liftdefl_of\<cdot>(defl TYPE('a))"
syntax "_DEFL" :: "type \<Rightarrow> logic" ("(1DEFL/(1'(_')))")
+syntax_consts "_DEFL" \<rightleftharpoons> defl
translations "DEFL('t)" \<rightleftharpoons> "CONST defl TYPE('t)"
instance "domain" \<subseteq> predomain
--- a/src/HOL/HOLCF/Sprod.thy Sun Aug 25 20:54:20 2024 +0200
+++ b/src/HOL/HOLCF/Sprod.thy Sun Aug 25 21:10:01 2024 +0200
@@ -41,6 +41,7 @@
where "ssplit = (\<Lambda> f p. seq\<cdot>p\<cdot>(f\<cdot>(sfst\<cdot>p)\<cdot>(ssnd\<cdot>p)))"
syntax "_stuple" :: "[logic, args] \<Rightarrow> logic" ("(1'(:_,/ _:'))")
+syntax_consts "_stuple" \<rightleftharpoons> spair
translations
"(:x, y, z:)" \<rightleftharpoons> "(:x, (:y, z:):)"
"(:x, y:)" \<rightleftharpoons> "CONST spair\<cdot>x\<cdot>y"
--- a/src/HOL/HOLCF/UpperPD.thy Sun Aug 25 20:54:20 2024 +0200
+++ b/src/HOL/HOLCF/UpperPD.thy Sun Aug 25 21:10:01 2024 +0200
@@ -134,6 +134,9 @@
syntax
"_upper_pd" :: "args \<Rightarrow> logic" ("{_}\<sharp>")
+syntax_consts
+ "_upper_pd" == upper_add
+
translations
"{x,xs}\<sharp>" == "{x}\<sharp> \<union>\<sharp> {xs}\<sharp>"
"{x}\<sharp>" == "CONST upper_unit\<cdot>x"
@@ -335,6 +338,9 @@
"_upper_bind" :: "[logic, logic, logic] \<Rightarrow> logic"
("(3\<Union>\<sharp>_\<in>_./ _)" [0, 0, 10] 10)
+syntax_consts
+ "_upper_bind" == upper_bind
+
translations
"\<Union>\<sharp>x\<in>xs. e" == "CONST upper_bind\<cdot>xs\<cdot>(\<Lambda> x. e)"
--- a/src/HOL/HOLCF/ex/Letrec.thy Sun Aug 25 20:54:20 2024 +0200
+++ b/src/HOL/HOLCF/ex/Letrec.thy Sun Aug 25 21:10:01 2024 +0200
@@ -22,6 +22,9 @@
"_recbinds" :: "[recbindt, recbinds] \<Rightarrow> recbinds" ("_;/ _")
"_Letrec" :: "[recbinds, logic] \<Rightarrow> logic" ("(Letrec (_)/ in (_))" 10)
+syntax_consts
+ "_recbind" "_recbinds" "_recbindt" "_Letrec" == CLetrec
+
translations
(recbindt) "x = a, (y,ys) = (b,bs)" == (recbindt) "(x,y,ys) = (a,b,bs)"
(recbindt) "x = a, y = b" == (recbindt) "(x,y) = (a,b)"
--- a/src/HOL/Library/Cardinality.thy Sun Aug 25 20:54:20 2024 +0200
+++ b/src/HOL/Library/Cardinality.thy Sun Aug 25 21:10:01 2024 +0200
@@ -32,6 +32,8 @@
syntax "_type_card" :: "type => nat" ("(1CARD/(1'(_')))")
+syntax_consts "_type_card" == card
+
translations "CARD('t)" => "CONST card (CONST UNIV :: 't set)"
print_translation \<open>
--- a/src/HOL/Library/FSet.thy Sun Aug 25 20:54:20 2024 +0200
+++ b/src/HOL/Library/FSet.thy Sun Aug 25 21:10:01 2024 +0200
@@ -167,6 +167,9 @@
syntax
"_insert_fset" :: "args => 'a fset" ("{|(_)|}")
+syntax_consts
+ "_insert_fset" == finsert
+
translations
"{|x, xs|}" == "CONST finsert x {|xs|}"
"{|x|}" == "CONST finsert x {||}"
@@ -200,6 +203,10 @@
"_fBall" :: "pttrn \<Rightarrow> 'a fset \<Rightarrow> bool \<Rightarrow> bool" ("(3\<forall>(_/|\<in>|_)./ _)" [0, 0, 10] 10)
"_fBex" :: "pttrn \<Rightarrow> 'a fset \<Rightarrow> bool \<Rightarrow> bool" ("(3\<exists>(_/|\<in>|_)./ _)" [0, 0, 10] 10)
+syntax_consts
+ "_fBall" \<rightleftharpoons> FSet.Ball and
+ "_fBex" \<rightleftharpoons> FSet.Bex
+
translations
"\<forall>x|\<in>|A. P" \<rightleftharpoons> "CONST FSet.Ball A (\<lambda>x. P)"
"\<exists>x|\<in>|A. P" \<rightleftharpoons> "CONST FSet.Bex A (\<lambda>x. P)"
--- a/src/HOL/Library/FuncSet.thy Sun Aug 25 20:54:20 2024 +0200
+++ b/src/HOL/Library/FuncSet.thy Sun Aug 25 21:10:01 2024 +0200
@@ -25,6 +25,9 @@
syntax
"_Pi" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set" ("(3\<Pi> _\<in>_./ _)" 10)
"_lam" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)" ("(3\<lambda>_\<in>_./ _)" [0,0,3] 3)
+syntax_consts
+ "_Pi" \<rightleftharpoons> Pi and
+ "_lam" \<rightleftharpoons> restrict
translations
"\<Pi> x\<in>A. B" \<rightleftharpoons> "CONST Pi A (\<lambda>x. B)"
"\<lambda>x\<in>A. f" \<rightleftharpoons> "CONST restrict (\<lambda>x. f) A"
@@ -350,6 +353,8 @@
syntax
"_PiE" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set" ("(3\<Pi>\<^sub>E _\<in>_./ _)" 10)
+syntax_consts
+ "_PiE" \<rightleftharpoons> Pi\<^sub>E
translations
"\<Pi>\<^sub>E x\<in>A. B" \<rightleftharpoons> "CONST Pi\<^sub>E A (\<lambda>x. B)"
--- a/src/HOL/Library/Groups_Big_Fun.thy Sun Aug 25 20:54:20 2024 +0200
+++ b/src/HOL/Library/Groups_Big_Fun.thy Sun Aug 25 21:10:01 2024 +0200
@@ -202,6 +202,8 @@
"_Sum_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add" ("(3SUM _. _)" [0, 10] 10)
syntax
"_Sum_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add" ("(3\<Sum>_. _)" [0, 10] 10)
+syntax_consts
+ "_Sum_any" \<rightleftharpoons> Sum_any
translations
"\<Sum>a. b" \<rightleftharpoons> "CONST Sum_any (\<lambda>a. b)"
@@ -255,6 +257,8 @@
"_Prod_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult" ("(3PROD _. _)" [0, 10] 10)
syntax
"_Prod_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult" ("(3\<Prod>_. _)" [0, 10] 10)
+syntax_consts
+ "_Prod_any" == Prod_any
translations
"\<Prod>a. b" == "CONST Prod_any (\<lambda>a. b)"
--- a/src/HOL/Library/Monad_Syntax.thy Sun Aug 25 20:54:20 2024 +0200
+++ b/src/HOL/Library/Monad_Syntax.thy Sun Aug 25 21:10:01 2024 +0200
@@ -46,6 +46,11 @@
"_do_bind" :: "[pttrn, 'a] \<Rightarrow> do_bind" ("(2_ <-/ _)" 13)
"_thenM" :: "['a, 'b] \<Rightarrow> 'c" (infixl ">>" 54)
+syntax_consts
+ "_do_block" "_do_cons" \<rightleftharpoons> bind_do and
+ "_do_bind" "_thenM" \<rightleftharpoons> bind and
+ "_do_let" \<rightleftharpoons> Let
+
translations
"_do_block (_do_cons (_do_then t) (_do_final e))"
\<rightleftharpoons> "CONST bind_do t (\<lambda>_. e)"
--- a/src/HOL/Library/Multiset.thy Sun Aug 25 20:54:20 2024 +0200
+++ b/src/HOL/Library/Multiset.thy Sun Aug 25 21:10:01 2024 +0200
@@ -93,6 +93,8 @@
syntax
"_multiset" :: "args \<Rightarrow> 'a multiset" ("{#(_)#}")
+syntax_consts
+ "_multiset" == add_mset
translations
"{#x, xs#}" == "CONST add_mset x {#xs#}"
"{#x#}" == "CONST add_mset x {#}"
@@ -169,6 +171,10 @@
"_MBall" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool" ("(3\<forall>_:#_./ _)" [0, 0, 10] 10)
"_MBex" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool" ("(3\<exists>_:#_./ _)" [0, 0, 10] 10)
+syntax_consts
+ "_MBall" \<rightleftharpoons> Multiset.Ball and
+ "_MBex" \<rightleftharpoons> Multiset.Bex
+
translations
"\<forall>x\<in>#A. P" \<rightleftharpoons> "CONST Multiset.Ball A (\<lambda>x. P)"
"\<exists>x\<in>#A. P" \<rightleftharpoons> "CONST Multiset.Bex A (\<lambda>x. P)"
@@ -1248,6 +1254,8 @@
"_MCollect" :: "pttrn \<Rightarrow> 'a multiset \<Rightarrow> bool \<Rightarrow> 'a multiset" ("(1{#_ :# _./ _#})")
syntax
"_MCollect" :: "pttrn \<Rightarrow> 'a multiset \<Rightarrow> bool \<Rightarrow> 'a multiset" ("(1{#_ \<in># _./ _#})")
+syntax_consts
+ "_MCollect" == filter_mset
translations
"{#x \<in># M. P#}" == "CONST filter_mset (\<lambda>x. P) M"
@@ -1821,6 +1829,8 @@
"_comprehension_mset" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> 'a multiset" ("({#_/. _ :# _#})")
syntax
"_comprehension_mset" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> 'a multiset" ("({#_/. _ \<in># _#})")
+syntax_consts
+ "_comprehension_mset" \<rightleftharpoons> image_mset
translations
"{#e. x \<in># M#}" \<rightleftharpoons> "CONST image_mset (\<lambda>x. e) M"
@@ -1828,6 +1838,8 @@
"_comprehension_mset'" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> bool \<Rightarrow> 'a multiset" ("({#_/ | _ :# _./ _#})")
syntax
"_comprehension_mset'" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> bool \<Rightarrow> 'a multiset" ("({#_/ | _ \<in># _./ _#})")
+syntax_consts
+ "_comprehension_mset'" \<rightleftharpoons> image_mset
translations
"{#e | x\<in>#M. P#}" \<rightharpoonup> "{#e. x \<in># {# x\<in>#M. P#}#}"
@@ -2675,6 +2687,8 @@
"_sum_mset_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add" ("(3SUM _:#_. _)" [0, 51, 10] 10)
syntax
"_sum_mset_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add" ("(3\<Sum>_\<in>#_. _)" [0, 51, 10] 10)
+syntax_consts
+ "_sum_mset_image" \<rightleftharpoons> sum_mset
translations
"\<Sum>i \<in># A. b" \<rightleftharpoons> "CONST sum_mset (CONST image_mset (\<lambda>i. b) A)"
@@ -2854,6 +2868,8 @@
"_prod_mset_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult" ("(3PROD _:#_. _)" [0, 51, 10] 10)
syntax
"_prod_mset_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult" ("(3\<Prod>_\<in>#_. _)" [0, 51, 10] 10)
+syntax_consts
+ "_prod_mset_image" \<rightleftharpoons> prod_mset
translations
"\<Prod>i \<in># A. b" \<rightleftharpoons> "CONST prod_mset (CONST image_mset (\<lambda>i. b) A)"
--- a/src/HOL/Library/Numeral_Type.thy Sun Aug 25 20:54:20 2024 +0200
+++ b/src/HOL/Library/Numeral_Type.thy Sun Aug 25 21:10:01 2024 +0200
@@ -540,6 +540,10 @@
"_NumeralType0" :: type ("0")
"_NumeralType1" :: type ("1")
+syntax_types
+ "_NumeralType0" == num0 and
+ "_NumeralType1" == num1
+
translations
(type) "1" == (type) "num1"
(type) "0" == (type) "num0"
--- a/src/HOL/Library/Phantom_Type.thy Sun Aug 25 20:54:20 2024 +0200
+++ b/src/HOL/Library/Phantom_Type.thy Sun Aug 25 21:10:01 2024 +0200
@@ -18,6 +18,7 @@
by(simp_all add: o_def id_def)
syntax "_Phantom" :: "type \<Rightarrow> logic" ("(1Phantom/(1'(_')))")
+syntax_consts "_Phantom" == phantom
translations
"Phantom('t)" => "CONST phantom :: _ \<Rightarrow> ('t, _) phantom"
--- a/src/HOL/Library/Type_Length.thy Sun Aug 25 20:54:20 2024 +0200
+++ b/src/HOL/Library/Type_Length.thy Sun Aug 25 21:10:01 2024 +0200
@@ -19,6 +19,9 @@
syntax "_type_length" :: "type \<Rightarrow> nat" (\<open>(1LENGTH/(1'(_')))\<close>)
+syntax_consts
+ "_type_length" \<rightleftharpoons> len_of
+
translations "LENGTH('a)" \<rightharpoonup>
"CONST len_of (CONST Pure.type :: 'a itself)"
--- a/src/HOL/Metis_Examples/Message.thy Sun Aug 25 20:54:20 2024 +0200
+++ b/src/HOL/Metis_Examples/Message.thy Sun Aug 25 21:10:01 2024 +0200
@@ -50,6 +50,8 @@
text\<open>Concrete syntax: messages appear as \<open>\<lbrace>A,B,NA\<rbrace>\<close>, etc...\<close>
syntax
"_MTuple" :: "['a, args] => 'a * 'b" ("(2\<lbrace>_,/ _\<rbrace>)")
+syntax_consts
+ "_MTuple" == MPair
translations
"\<lbrace>x, y, z\<rbrace>" == "\<lbrace>x, \<lbrace>y, z\<rbrace>\<rbrace>"
"\<lbrace>x, y\<rbrace>" == "CONST MPair x y"
--- a/src/HOL/Probability/Fin_Map.thy Sun Aug 25 20:54:20 2024 +0200
+++ b/src/HOL/Probability/Fin_Map.thy Sun Aug 25 21:10:01 2024 +0200
@@ -90,6 +90,8 @@
syntax
"_Pi'" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3\<Pi>'' _\<in>_./ _)" 10)
+syntax_consts
+ "_Pi'" == Pi'
translations
"\<Pi>' x\<in>A. B" == "CONST Pi' A (\<lambda>x. B)"
@@ -635,6 +637,8 @@
syntax
"_PiF" :: "pttrn \<Rightarrow> 'i set \<Rightarrow> 'a measure \<Rightarrow> ('i => 'a) measure" ("(3\<Pi>\<^sub>F _\<in>_./ _)" 10)
+syntax_consts
+ "_PiF" == PiF
translations
"\<Pi>\<^sub>F x\<in>I. M" == "CONST PiF I (%x. M)"
--- a/src/HOL/Probability/Probability_Measure.thy Sun Aug 25 20:54:20 2024 +0200
+++ b/src/HOL/Probability/Probability_Measure.thy Sun Aug 25 21:10:01 2024 +0200
@@ -250,6 +250,9 @@
syntax
"_prob" :: "pttrn \<Rightarrow> logic \<Rightarrow> logic \<Rightarrow> logic" (\<open>('\<P>'((/_ in _./ _)'))\<close>)
+syntax_consts
+ "_prob" == measure
+
translations
"\<P>(x in M. P)" => "CONST measure M {x \<in> CONST space M. P}"
@@ -322,6 +325,9 @@
syntax
"_conditional_prob" :: "pttrn \<Rightarrow> logic \<Rightarrow> logic \<Rightarrow> logic \<Rightarrow> logic" (\<open>('\<P>'(_ in _. _ \<bar>/ _'))\<close>)
+syntax_consts
+ "_conditional_prob" == cond_prob
+
translations
"\<P>(x in M. P \<bar> Q)" => "CONST cond_prob M (\<lambda>x. P) (\<lambda>x. Q)"
--- a/src/HOL/Quotient_Examples/Lift_FSet.thy Sun Aug 25 20:54:20 2024 +0200
+++ b/src/HOL/Quotient_Examples/Lift_FSet.thy Sun Aug 25 21:10:01 2024 +0200
@@ -98,6 +98,9 @@
syntax
"_insert_fset" :: "args => 'a fset" ("{|(_)|}")
+syntax_consts
+ "_insert_fset" == fcons
+
translations
"{|x, xs|}" == "CONST fcons x {|xs|}"
"{|x|}" == "CONST fcons x {||}"
--- a/src/HOL/Quotient_Examples/Quotient_FSet.thy Sun Aug 25 20:54:20 2024 +0200
+++ b/src/HOL/Quotient_Examples/Quotient_FSet.thy Sun Aug 25 21:10:01 2024 +0200
@@ -291,6 +291,9 @@
syntax
"_insert_fset" :: "args => 'a fset" ("{|(_)|}")
+syntax_consts
+ "_insert_fset" == insert_fset
+
translations
"{|x, xs|}" == "CONST insert_fset x {|xs|}"
"{|x|}" == "CONST insert_fset x {||}"
--- a/src/HOL/SET_Protocol/Message_SET.thy Sun Aug 25 20:54:20 2024 +0200
+++ b/src/HOL/SET_Protocol/Message_SET.thy Sun Aug 25 21:10:01 2024 +0200
@@ -70,6 +70,8 @@
(*Concrete syntax: messages appear as \<open>\<lbrace>A,B,NA\<rbrace>\<close>, etc...*)
syntax
"_MTuple" :: "['a, args] \<Rightarrow> 'a * 'b" ("(2\<lbrace>_,/ _\<rbrace>)")
+syntax_consts
+ "_MTuple" == MPair
translations
"\<lbrace>x, y, z\<rbrace>" == "\<lbrace>x, \<lbrace>y, z\<rbrace>\<rbrace>"
"\<lbrace>x, y\<rbrace>" == "CONST MPair x y"
--- a/src/HOL/SPARK/SPARK_Setup.thy Sun Aug 25 20:54:20 2024 +0200
+++ b/src/HOL/SPARK/SPARK_Setup.thy Sun Aug 25 21:10:01 2024 +0200
@@ -57,6 +57,9 @@
syntax
"_updsbind" :: "['a, 'a] => updbind" ("(2_ [:=]/ _)")
+syntax_consts
+ "_updsbind" == fun_upds
+
translations
"f(xs[:=]y)" == "CONST fun_upds f xs y"
--- a/src/HOL/UNITY/PPROD.thy Sun Aug 25 20:54:20 2024 +0200
+++ b/src/HOL/UNITY/PPROD.thy Sun Aug 25 21:10:01 2024 +0200
@@ -16,6 +16,8 @@
syntax
"_PLam" :: "[pttrn, nat set, 'b set] => (nat => 'b) set" ("(3plam _:_./ _)" 10)
+syntax_consts
+ "_PLam" == PLam
translations
"plam x : A. B" == "CONST PLam A (%x. B)"
--- a/src/HOL/UNITY/Union.thy Sun Aug 25 20:54:20 2024 +0200
+++ b/src/HOL/UNITY/Union.thy Sun Aug 25 21:10:01 2024 +0200
@@ -41,6 +41,8 @@
syntax
"_JOIN1" :: "[pttrns, 'b set] => 'b set" ("(3\<Squnion>_./ _)" 10)
"_JOIN" :: "[pttrn, 'a set, 'b set] => 'b set" ("(3\<Squnion>_\<in>_./ _)" 10)
+syntax_consts
+ "_JOIN1" "_JOIN" == JOIN
translations
"\<Squnion>x \<in> A. B" == "CONST JOIN A (\<lambda>x. B)"
"\<Squnion>x y. B" == "\<Squnion>x. \<Squnion>y. B"
--- a/src/HOL/ex/Code_Lazy_Demo.thy Sun Aug 25 20:54:20 2024 +0200
+++ b/src/HOL/ex/Code_Lazy_Demo.thy Sun Aug 25 21:10:01 2024 +0200
@@ -40,6 +40,7 @@
| LCons (lhd: 'a) (ltl: "'a llist") (infixr "###" 65)
syntax "_llist" :: "args => 'a list" ("\<^bold>\<lbrakk>(_)\<^bold>\<rbrakk>")
+syntax_consts "_llist" == LCons
translations
"\<^bold>\<lbrakk>x, xs\<^bold>\<rbrakk>" == "x###\<^bold>\<lbrakk>xs\<^bold>\<rbrakk>"
"\<^bold>\<lbrakk>x\<^bold>\<rbrakk>" == "x###\<^bold>\<lbrakk>\<^bold>\<rbrakk>"
--- a/src/Pure/Examples/Higher_Order_Logic.thy Sun Aug 25 20:54:20 2024 +0200
+++ b/src/Pure/Examples/Higher_Order_Logic.thy Sun Aug 25 21:10:01 2024 +0200
@@ -402,6 +402,7 @@
where someI: "P x \<Longrightarrow> P (Eps P)"
syntax "_Eps" :: "pttrn \<Rightarrow> o \<Rightarrow> 'a" ("(3SOME _./ _)" [0, 10] 10)
+syntax_consts "_Eps" \<rightleftharpoons> Eps
translations "SOME x. P" \<rightleftharpoons> "CONST Eps (\<lambda>x. P)"
text \<open>