# HG changeset patch # User wenzelm # Date 1724613001 -7200 # Node ID c7723cc15de8c8d8e5341d06bb586d16c9d92913 # Parent 079fe4292526a2d458f06dfd93ba94a922354e3a more markup for syntax consts; diff -r 079fe4292526 -r c7723cc15de8 src/Benchmarks/Quickcheck_Benchmark/Needham_Schroeder_Base.thy --- 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\_,/ _\)") +syntax_consts + "_MTuple" == MPair translations "\x, y, z\" == "\x, \y, z\\" "\x, y\" == "CONST MPair x y" diff -r 079fe4292526 -r c7723cc15de8 src/Doc/Tutorial/Protocol/Message.thy --- 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\Concrete syntax: messages appear as \\A,B,NA\\, etc...\ syntax "_MTuple" :: "['a, args] \ 'a * 'b" ("(2\_,/ _\)") +syntax_consts + "_MTuple" == MPair translations "\x, y, z\" == "\x, \y, z\\" "\x, y\" == "CONST MPair x y" diff -r 079fe4292526 -r c7723cc15de8 src/HOL/Algebra/FiniteProduct.thy --- 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 \ idt \ 'a set \ 'b \ 'b" ("(3\__\_. _)" [1000, 0, 51, 10] 10) +syntax_consts + "_finprod" \ finprod translations "\\<^bsub>G\<^esub>i\A. b" \ "CONST finprod G (%i. b) A" \ \Beware of argument permutation!\ diff -r 079fe4292526 -r c7723cc15de8 src/HOL/Algebra/Lattice.thy --- 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 \ pttrns \ 'a \ 'a" ("(3SSUP\ _./ _)" [0, 10] 10) "_sup" :: "('a, 'b) gorder_scheme \ pttrn \ 'c set \ 'a \ 'a" ("(3SSUP\ _:_./ _)" [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)" diff -r 079fe4292526 -r c7723cc15de8 src/HOL/Algebra/Ring.thy --- 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 \ idt \ 'a set \ 'b \ 'b" ("(3\__\_. _)" [1000, 0, 51, 10] 10) +syntax_consts + "_finsum" \ finsum translations "\\<^bsub>G\<^esub>i\A. b" \ "CONST finsum G (\i. b) A" \ \Beware of argument permutation!\ diff -r 079fe4292526 -r c7723cc15de8 src/HOL/Analysis/Bochner_Integration.thy --- 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 \ real \ 'a measure \ real" ("\((2 _./ _)/ \_)" [60,61] 110) +syntax_consts + "_lebesgue_integral" == lebesgue_integral + translations "\ x. f \M" == "CONST lebesgue_integral M (\x. f)" syntax "_ascii_lebesgue_integral" :: "pttrn \ 'a measure \ real \ real" ("(3LINT (1_)/|(_)./ _)" [0,110,60] 60) +syntax_consts + "_ascii_lebesgue_integral" == lebesgue_integral + translations "LINT x|M. f" == "CONST lebesgue_integral M (\x. f)" diff -r 079fe4292526 -r c7723cc15de8 src/HOL/Analysis/Euclidean_Space.thy --- 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 @@ "(\u\Basis. inner x u = 0) \ (x = 0)" syntax "_type_dimension" :: "type \ nat" ("(1DIM/(1'(_')))") +syntax_consts "_type_dimension" \ card translations "DIM('a)" \ "CONST card (CONST Basis :: 'a set)" typed_print_translation \ [(\<^const_syntax>\card\, diff -r 079fe4292526 -r c7723cc15de8 src/HOL/Analysis/Finite_Cartesian_Product.thy --- 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> \'a^'b::_\ becomes \('a, 'b) vec\ without extra sort-constraint \ syntax "_vec_type" :: "type \ type \ type" (infixl "^" 15) +syntax_types "_vec_type" \ vec parse_translation \ let fun vec t u = Syntax.const \<^type_syntax>\vec\ $ t $ u; diff -r 079fe4292526 -r c7723cc15de8 src/HOL/Analysis/Finite_Product_Measure.thy --- 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 \ 'i set \ 'a measure \ ('i => 'a) measure" ("(3\\<^sub>M _\_./ _)" 10) +syntax_consts + "_PiM" == PiM translations "\\<^sub>M x\I. M" == "CONST PiM I (%x. M)" diff -r 079fe4292526 -r c7723cc15de8 src/HOL/Analysis/Infinite_Set_Sum.thy --- 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 \ 'a set \ 'b \ 'b::{banach, second_countable_topology}" ("(2\\<^sub>a_\_./ _)" [0, 51, 10] 10) +syntax_consts + "_infsetsum" \ infsetsum translations \ \Beware of argument permutation!\ "\\<^sub>ai\A. b" \ "CONST infsetsum (\i. b) A" @@ -109,6 +111,8 @@ syntax "_uinfsetsum" :: "pttrn \ 'b \ 'b::{banach, second_countable_topology}" ("(2\\<^sub>a_./ _)" [0, 10] 10) +syntax_consts + "_uinfsetsum" \ infsetsum translations \ \Beware of argument permutation!\ "\\<^sub>ai. b" \ "CONST infsetsum (\i. b) (CONST UNIV)" @@ -118,6 +122,8 @@ syntax "_qinfsetsum" :: "pttrn \ bool \ 'a \ 'a::{banach, second_countable_topology}" ("(2\\<^sub>a_ | (_)./ _)" [0, 0, 10] 10) +syntax_consts + "_qinfsetsum" \ infsetsum translations "\\<^sub>ax|P. t" => "CONST infsetsum (\x. t) {x. P}" diff -r 079fe4292526 -r c7723cc15de8 src/HOL/Analysis/Infinite_Sum.thy --- 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 \ 'a set \ 'b \ 'b::topological_comm_monoid_add" ("(3INFSUM (_/:_)./ _)" [0, 51, 10] 10) syntax "_infsum" :: "pttrn \ 'a set \ 'b \ 'b::topological_comm_monoid_add" ("(2\\<^sub>\(_/\_)./ _)" [0, 51, 10] 10) +syntax_consts + "_infsum" \ infsum translations \ \Beware of argument permutation!\ "\\<^sub>\i\A. b" \ "CONST infsum (\i. b) A" @@ -57,6 +59,8 @@ "_univinfsum" :: "pttrn \ 'a \ 'a" ("(3INFSUM _./ _)" [0, 10] 10) syntax "_univinfsum" :: "pttrn \ 'a \ 'a" ("(2\\<^sub>\_./ _)" [0, 10] 10) +syntax_consts + "_univinfsum" \ infsum translations "\\<^sub>\x. t" \ "CONST infsum (\x. t) (CONST UNIV)" @@ -64,6 +68,8 @@ "_qinfsum" :: "pttrn \ bool \ 'a \ 'a" ("(3INFSUM _ |/ _./ _)" [0, 0, 10] 10) syntax "_qinfsum" :: "pttrn \ bool \ 'a \ 'a" ("(2\\<^sub>\_ | (_)./ _)" [0, 0, 10] 10) +syntax_consts + "_qinfsum" \ infsum translations "\\<^sub>\x|P. t" => "CONST infsum (\x. t) {x. P}" diff -r 079fe4292526 -r c7723cc15de8 src/HOL/Analysis/Interval_Integral.thy --- 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 \ real \ real \ real measure \ real \ 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 (\x. f)" @@ -159,6 +162,9 @@ "_ascii_interval_lebesgue_borel_integral" :: "pttrn \ real \ real \ real \ 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 (\x. f)" @@ -1045,11 +1051,17 @@ syntax "_complex_lebesgue_borel_integral" :: "pttrn \ real \ complex" ("(2CLBINT _. _)" [0,60] 60) +syntax_consts + "_complex_lebesgue_borel_integral" == complex_lebesgue_integral + translations "CLBINT x. f" == "CONST complex_lebesgue_integral CONST lborel (\x. f)" syntax "_complex_set_lebesgue_borel_integral" :: "pttrn \ real set \ real \ 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 (\x. f)" @@ -1065,6 +1077,9 @@ "_ascii_complex_interval_lebesgue_borel_integral" :: "pttrn \ ereal \ ereal \ real \ 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 (\x. f)" diff -r 079fe4292526 -r c7723cc15de8 src/HOL/Analysis/Measure_Space.thy --- 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 \ 'a \ bool \ bool" ("AE _ in _. _" [0,0,10] 10) +syntax_consts + "_almost_everywhere" \ almost_everywhere + translations "AE x in M. P" \ "CONST almost_everywhere M (\x. P)" @@ -1016,6 +1019,9 @@ "_set_almost_everywhere" :: "pttrn \ 'a set \ 'a \ bool \ bool" ("AE _\_ in _./ _" [0,0,0,10] 10) +syntax_consts + "_set_almost_everywhere" \ set_almost_everywhere + translations "AE x\A in M. P" \ "CONST set_almost_everywhere A M (\x. P)" diff -r 079fe4292526 -r c7723cc15de8 src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy --- 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 \ ennreal \ 'a measure \ ennreal" ("\\<^sup>S _. _ \_" [60,61] 110) +syntax_consts + "_simple_integral" == simple_integral + translations "\\<^sup>S x. f \M" == "CONST simple_integral M (%x. f)" @@ -819,6 +822,9 @@ syntax "_nn_integral" :: "pttrn \ ennreal \ 'a measure \ ennreal" ("\\<^sup>+((2 _./ _)/ \_)" [60,61] 110) +syntax_consts + "_nn_integral" == nn_integral + translations "\\<^sup>+x. f \M" == "CONST nn_integral M (\x. f)" diff -r 079fe4292526 -r c7723cc15de8 src/HOL/Analysis/Set_Integral.thy --- 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 \ 'a set \ 'a measure \ real \ 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 (\x. f)" @@ -576,6 +579,9 @@ "_complex_lebesgue_integral" :: "pttrn \ complex \ 'a measure \ complex" ("\\<^sup>C _. _ \_" [0,0] 110) +syntax_consts + "_complex_lebesgue_integral" == complex_lebesgue_integral + translations "\\<^sup>Cx. f \M" == "CONST complex_lebesgue_integral M (\x. f)" @@ -583,6 +589,9 @@ "_ascii_complex_lebesgue_integral" :: "pttrn \ 'a measure \ real \ 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 (\x. f)" @@ -617,6 +626,9 @@ "_ascii_complex_set_lebesgue_integral" :: "pttrn \ 'a set \ 'a measure \ real \ 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 (\x. f)" @@ -640,6 +652,10 @@ "_set_lebesgue_integral" :: "pttrn => 'a set => 'a measure => ereal => ereal" ("(\((_)\(_)./ _)/\_)" [0,0,0,110] 10) +syntax_consts +"_set_nn_integral" == set_nn_integral and +"_set_lebesgue_integral" == set_lebesgue_integral + translations "\\<^sup>+x \ A. f \M" == "CONST set_nn_integral M A (\x. f)" "\x \ A. f \M" == "CONST set_lebesgue_integral M A (\x. f)" diff -r 079fe4292526 -r c7723cc15de8 src/HOL/Analysis/Sparse_In.thy --- 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\\<^sub>\_\_./ _)" [0, 0, 10] 10) +syntax_consts + "_eventually_cosparse" == eventually translations "\\<^sub>\x\A. P" == "CONST eventually (\x. P) (CONST cosparse A)" syntax "_qeventually_cosparse" :: "pttrn \ bool \ 'a \ 'a" ("(3\\<^sub>\_ | (_)./ _)" [0, 0, 10] 10) +syntax_consts + "_qeventually_cosparse" == eventually translations "\\<^sub>\x|P. t" => "CONST eventually (\x. t) (CONST cosparse {x. P})" diff -r 079fe4292526 -r c7723cc15de8 src/HOL/Auth/Message.thy --- 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\Concrete syntax: messages appear as \\A,B,NA\\, etc...\ syntax "_MTuple" :: "['a, args] \ 'a * 'b" ("(2\_,/ _\)") +syntax_consts + "_MTuple" \ MPair translations "\x, y, z\" \ "\x, \y, z\\" "\x, y\" \ "CONST MPair x y" diff -r 079fe4292526 -r c7723cc15de8 src/HOL/Bali/AxSem.thy --- 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 \ 'a assn \ 'a assn" ("\_:. _" [0,3] 3) +syntax_consts + "_peek_res" == peek_res translations "\w:. P" == "CONST peek_res (\w. P)" @@ -266,6 +268,8 @@ syntax "_peek_st" :: "pttrn \ 'a assn \ 'a assn" ("\_.. _" [0,3] 3) +syntax_consts + "_peek_st" == peek_st translations "\s.. P" == "CONST peek_st (\s. P)" diff -r 079fe4292526 -r c7723cc15de8 src/HOL/Bali/Basis.thy --- 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] \ bool" ("(3\_\_:/ _)" [0,0,10] 10) "_Oex" :: "[pttrn, 'a option, bool] \ bool" ("(3\_\_:/ _)" [0,0,10] 10) +syntax_consts + "_Oall" \ Ball and + "_Oex" \ Bex + translations "\x\A: P" \ "\x\CONST set_option A. P" "\x\A: P" \ "\x\CONST set_option A. P" @@ -257,6 +261,8 @@ text \list patterns -- extends pre-defined type "pttrn" used in abstractions\ syntax "_lpttrn" :: "[pttrn, pttrn] \ pttrn" ("_#/_" [901,900] 900) +syntax_consts + "_lpttrn" \ lsplit translations "\y # x # xs. b" \ "CONST lsplit (\y x # xs. b)" "\x # xs. b" \ "CONST lsplit (\x xs. b)" diff -r 079fe4292526 -r c7723cc15de8 src/HOL/Bali/State.thy --- 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 \ oref" Stat :: "qtname \ oref" +syntax_consts + Heap == Inl and + Stat == Inr + translations "Heap" => "CONST Inl" "Stat" => "CONST Inr" diff -r 079fe4292526 -r c7723cc15de8 src/HOL/Codegenerator_Test/Code_Lazy_Test.thy --- 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>]" diff -r 079fe4292526 -r c7723cc15de8 src/HOL/HOLCF/Cfun.thy --- 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] \ logic" ("(3\ _./ _)" [1000, 10] 10) +syntax_consts + "_Lambda" \ Abs_cfun + parse_ast_translation \ (* 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 *) diff -r 079fe4292526 -r c7723cc15de8 src/HOL/HOLCF/ConvexPD.thy --- 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 \ logic" ("{_}\") +syntax_consts + "_convex_pd" == convex_add + translations "{x,xs}\" == "{x}\ \\ {xs}\" "{x}\" == "CONST convex_unit\x" @@ -348,6 +351,9 @@ "_convex_bind" :: "[logic, logic, logic] \ logic" ("(3\\_\_./ _)" [0, 0, 10] 10) +syntax_consts + "_convex_bind" == convex_bind + translations "\\x\xs. e" == "CONST convex_bind\xs\(\ x. e)" diff -r 079fe4292526 -r c7723cc15de8 src/HOL/HOLCF/IOA/Sequence.thy --- 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 \ 'a Seq" ("[(_)!]") "_partlist" :: "args \ 'a Seq" ("[(_)?]") +syntax_consts + "_totlist" "_partlist" \ Consq translations "[x, xs!]" \ "x \ [xs!]" "[x!]" \ "x\nil" diff -r 079fe4292526 -r c7723cc15de8 src/HOL/HOLCF/LowerPD.thy --- 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 \ logic" ("{_}\") +syntax_consts + "_lower_pd" == lower_add + translations "{x,xs}\" == "{x}\ \\ {xs}\" "{x}\" == "CONST lower_unit\x" @@ -342,6 +345,9 @@ "_lower_bind" :: "[logic, logic, logic] \ logic" ("(3\\_\_./ _)" [0, 0, 10] 10) +syntax_consts + "_lower_bind" == lower_bind + translations "\\x\xs. e" == "CONST lower_bind\xs\(\ x. e)" diff -r 079fe4292526 -r c7723cc15de8 src/HOL/HOLCF/Pcpo.thy --- 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 \Old "UU" syntax:\ syntax UU :: logic +syntax_consts UU \ bottom translations "UU" \ "CONST bottom" text \Simproc to rewrite \<^term>\\ = x\ to \<^term>\x = \\.\ diff -r 079fe4292526 -r c7723cc15de8 src/HOL/HOLCF/Porder.thy --- 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] \ 'b" ("(3\_\_./ _)" [0,0, 10] 10) +syntax_consts + "_BLub" \ lub + translations "LUB x:A. t" \ "CONST lub ((\