# HG changeset patch # User wenzelm # Date 1727807956 -7200 # Node ID c007e6d9941df278c5cd4b1588c1e5fdc46eedc6 # Parent 843dba3d307acc0e41fefa17300459e2a80abc1e drop somewhat pointless 'syntax_consts' declarations; diff -r 843dba3d307a -r c007e6d9941d src/Benchmarks/Quickcheck_Benchmark/Needham_Schroeder_Base.thy --- a/src/Benchmarks/Quickcheck_Benchmark/Needham_Schroeder_Base.thy Mon Sep 30 23:32:26 2024 +0200 +++ b/src/Benchmarks/Quickcheck_Benchmark/Needham_Schroeder_Base.thy Tue Oct 01 20:39:16 2024 +0200 @@ -28,8 +28,6 @@ syntax "_MTuple" :: "['a, args] \ 'a * 'b" (\(\indent=2 notation=\mixfix message tuple\\\_,/ _\)\) -syntax_consts - MPair translations "\x, y, z\" \ "\x, \y, z\\" "\x, y\" \ "CONST MPair x y" diff -r 843dba3d307a -r c007e6d9941d src/CCL/Set.thy --- a/src/CCL/Set.thy Mon Sep 30 23:32:26 2024 +0200 +++ b/src/CCL/Set.thy Tue Oct 01 20:39:16 2024 +0200 @@ -19,8 +19,6 @@ syntax "_Coll" :: "[idt, o] \ 'a set" (\(\indent=1 notation=\mixfix Collect\\{_./ _})\) -syntax_consts - Collect translations "{x. P}" == "CONST Collect(\x. P)" diff -r 843dba3d307a -r c007e6d9941d src/CCL/Term.thy --- a/src/CCL/Term.thy Mon Sep 30 23:32:26 2024 +0200 +++ b/src/CCL/Term.thy Tue Oct 01 20:39:16 2024 +0200 @@ -51,7 +51,6 @@ syntax "_let1" :: "[idt,i,i]\i" (\(\indent=3 notation=\mixfix let be in\\let _ be _/ in _)\ [0,0,60] 60) -syntax_consts let1 translations "let x be a in e" == "CONST let1(a, \x. e)" definition letrec :: "[[i,i\i]\i,(i\i)\i]\i" @@ -73,7 +72,6 @@ (\(\indent=3 notation=\mixfix letrec be in\\letrec _ _ _ be _/ in _)\ [0,0,0,0,60] 60) "_letrec3" :: "[idt,idt,idt,idt,i,i]\i" (\(\indent=3 notation=\mixfix letrec be in\\letrec _ _ _ _ be _/ in _)\ [0,0,0,0,0,60] 60) -syntax_consts letrec letrec2 letrec3 parse_translation \ let fun abs_tr t u = Syntax_Trans.abs_tr [t, u]; diff -r 843dba3d307a -r c007e6d9941d src/CCL/Type.thy --- a/src/CCL/Type.thy Mon Sep 30 23:32:26 2024 +0200 +++ b/src/CCL/Type.thy Tue Oct 01 20:39:16 2024 +0200 @@ -14,8 +14,6 @@ syntax "_Subtype" :: "[idt, 'a set, o] \ 'a set" (\(\indent=1 notation=\mixfix Subtype\\{_: _ ./ _})\) -syntax_consts - Subtype translations "{x: A. B}" == "CONST Subtype(A, \x. B)" diff -r 843dba3d307a -r c007e6d9941d src/Doc/Tutorial/Protocol/Message.thy --- a/src/Doc/Tutorial/Protocol/Message.thy Mon Sep 30 23:32:26 2024 +0200 +++ b/src/Doc/Tutorial/Protocol/Message.thy Tue Oct 01 20:39:16 2024 +0200 @@ -81,8 +81,6 @@ text\Concrete syntax: messages appear as \\A,B,NA\\, etc...\ syntax "_MTuple" :: "['a, args] \ 'a * 'b" ("(\indent=2 notation=\mixfix message tuple\\\_,/ _\)") -syntax_consts - MPair translations "\x, y, z\" \ "\x, \y, z\\" "\x, y\" \ "CONST MPair x y" diff -r 843dba3d307a -r c007e6d9941d src/FOL/IFOL.thy --- a/src/FOL/IFOL.thy Mon Sep 30 23:32:26 2024 +0200 +++ b/src/FOL/IFOL.thy Tue Oct 01 20:39:16 2024 +0200 @@ -747,8 +747,6 @@ "" :: \letbind => letbinds\ (\_\) "_binds" :: \[letbind, letbinds] => letbinds\ (\_;/ _\) "_Let" :: \[letbinds, 'a] => 'a\ (\(\notation=\mixfix let in\\let (_)/ in (_))\ 10) -syntax_consts - Let translations "_Let(_binds(b, bs), e)" == "_Let(b, _Let(bs, e))" "let x = a in e" == "CONST Let(a, \x. e)" diff -r 843dba3d307a -r c007e6d9941d src/HOL/Auth/Message.thy --- a/src/HOL/Auth/Message.thy Mon Sep 30 23:32:26 2024 +0200 +++ b/src/HOL/Auth/Message.thy Tue Oct 01 20:39:16 2024 +0200 @@ -51,8 +51,6 @@ text\Concrete syntax: messages appear as \\A,B,NA\\, etc...\ syntax "_MTuple" :: "['a, args] \ 'a * 'b" (\(\indent=2 notation=\mixfix message tuple\\\_,/ _\)\) -syntax_consts - MPair translations "\x, y, z\" \ "\x, \y, z\\" "\x, y\" \ "CONST MPair x y" diff -r 843dba3d307a -r c007e6d9941d src/HOL/Codegenerator_Test/Code_Lazy_Test.thy --- a/src/HOL/Codegenerator_Test/Code_Lazy_Test.thy Mon Sep 30 23:32:26 2024 +0200 +++ b/src/HOL/Codegenerator_Test/Code_Lazy_Test.thy Tue Oct 01 20:39:16 2024 +0200 @@ -25,8 +25,6 @@ no_notation lazy_llist (\_\) syntax "_llist" :: "args => 'a list" (\(\indent=1 notation=\mixfix lazy list enumeration\\\<^bold>[_\<^bold>])\) -syntax_consts - lazy_llist translations "\<^bold>[x, xs\<^bold>]" == "x\<^bold>#\<^bold>[xs\<^bold>]" "\<^bold>[x\<^bold>]" == "x\<^bold>#\<^bold>[\<^bold>]" diff -r 843dba3d307a -r c007e6d9941d src/HOL/Computational_Algebra/Polynomial.thy --- a/src/HOL/Computational_Algebra/Polynomial.thy Mon Sep 30 23:32:26 2024 +0200 +++ b/src/HOL/Computational_Algebra/Polynomial.thy Tue Oct 01 20:39:16 2024 +0200 @@ -350,8 +350,6 @@ syntax "_poly" :: "args \ 'a poly" (\(\indent=2 notation=\mixfix polynomial enumeration\\[:_:])\) -syntax_consts - pCons translations "[:x, xs:]" \ "CONST pCons x [:xs:]" "[:x:]" \ "CONST pCons x 0" diff -r 843dba3d307a -r c007e6d9941d src/HOL/Fun.thy --- a/src/HOL/Fun.thy Mon Sep 30 23:32:26 2024 +0200 +++ b/src/HOL/Fun.thy Tue Oct 01 20:39:16 2024 +0200 @@ -846,9 +846,6 @@ "_updbinds":: "updbind \ updbinds \ updbinds" (\_,/ _\) "_Update" :: "'a \ updbinds \ 'a" (\_/'((2_)')\ [1000, 0] 900) -syntax_consts - fun_upd - translations "_Update f (_updbinds b bs)" \ "_Update (_Update f b) bs" "f(x:=y)" \ "CONST fun_upd f x y" diff -r 843dba3d307a -r c007e6d9941d src/HOL/HOLCF/ConvexPD.thy --- a/src/HOL/HOLCF/ConvexPD.thy Mon Sep 30 23:32:26 2024 +0200 +++ b/src/HOL/HOLCF/ConvexPD.thy Tue Oct 01 20:39:16 2024 +0200 @@ -180,8 +180,6 @@ syntax "_convex_pd" :: "args \ logic" (\(\indent=1 notation=\mixfix convex_pd enumeration\\{_}\)\) -syntax_consts - convex_add translations "{x,xs}\" == "{x}\ \\ {xs}\" "{x}\" == "CONST convex_unit\x" diff -r 843dba3d307a -r c007e6d9941d src/HOL/HOLCF/IOA/Sequence.thy --- a/src/HOL/HOLCF/IOA/Sequence.thy Mon Sep 30 23:32:26 2024 +0200 +++ b/src/HOL/HOLCF/IOA/Sequence.thy Tue Oct 01 20:39:16 2024 +0200 @@ -72,8 +72,6 @@ syntax "_totlist" :: "args \ 'a Seq" (\(\indent=1 notation=\mixfix total list enumeration\\[_!])\) "_partlist" :: "args \ 'a Seq" (\(\indent=1 notation=\mixfix partial list enumeration\\[_?])\) -syntax_consts - Consq translations "[x, xs!]" \ "x \ [xs!]" "[x!]" \ "x\nil" diff -r 843dba3d307a -r c007e6d9941d src/HOL/HOLCF/LowerPD.thy --- a/src/HOL/HOLCF/LowerPD.thy Mon Sep 30 23:32:26 2024 +0200 +++ b/src/HOL/HOLCF/LowerPD.thy Tue Oct 01 20:39:16 2024 +0200 @@ -135,8 +135,6 @@ syntax "_lower_pd" :: "args \ logic" (\(\indent=1 notation=\mixfix lower_pd enumeration\\{_}\)\) -syntax_consts - lower_add translations "{x,xs}\" == "{x}\ \\ {xs}\" "{x}\" == "CONST lower_unit\x" diff -r 843dba3d307a -r c007e6d9941d src/HOL/HOLCF/Sprod.thy --- a/src/HOL/HOLCF/Sprod.thy Mon Sep 30 23:32:26 2024 +0200 +++ b/src/HOL/HOLCF/Sprod.thy Tue Oct 01 20:39:16 2024 +0200 @@ -42,8 +42,6 @@ syntax "_stuple" :: "[logic, args] \ logic" (\(\indent=1 notation=\mixfix strict tuple\\'(:_,/ _:'))\) -syntax_consts - spair translations "(:x, y, z:)" \ "(:x, (:y, z:):)" "(:x, y:)" \ "CONST spair\x\y" diff -r 843dba3d307a -r c007e6d9941d src/HOL/HOLCF/UpperPD.thy --- a/src/HOL/HOLCF/UpperPD.thy Mon Sep 30 23:32:26 2024 +0200 +++ b/src/HOL/HOLCF/UpperPD.thy Tue Oct 01 20:39:16 2024 +0200 @@ -133,8 +133,6 @@ syntax "_upper_pd" :: "args \ logic" (\(\indent=1 notation=\mixfix upper_pd enumeration\\{_}\)\) -syntax_consts - upper_add translations "{x,xs}\" == "{x}\ \\ {xs}\" "{x}\" == "CONST upper_unit\x" diff -r 843dba3d307a -r c007e6d9941d src/HOL/Library/FSet.thy --- a/src/HOL/Library/FSet.thy Mon Sep 30 23:32:26 2024 +0200 +++ b/src/HOL/Library/FSet.thy Tue Oct 01 20:39:16 2024 +0200 @@ -166,8 +166,6 @@ syntax "_fset" :: "args => 'a fset" (\(\indent=2 notation=\mixfix finite set enumeration\\{|_|})\) -syntax_consts - finsert translations "{|x, xs|}" == "CONST finsert x {|xs|}" "{|x|}" == "CONST finsert x {||}" diff -r 843dba3d307a -r c007e6d9941d src/HOL/Library/Multiset.thy --- a/src/HOL/Library/Multiset.thy Mon Sep 30 23:32:26 2024 +0200 +++ b/src/HOL/Library/Multiset.thy Tue Oct 01 20:39:16 2024 +0200 @@ -93,8 +93,6 @@ syntax "_multiset" :: "args \ 'a multiset" (\(\indent=2 notation=\mixfix multiset enumeration\\{#_#})\) -syntax_consts - add_mset translations "{#x, xs#}" == "CONST add_mset x {#xs#}" "{#x#}" == "CONST add_mset x {#}" diff -r 843dba3d307a -r c007e6d9941d src/HOL/List.thy --- a/src/HOL/List.thy Mon Sep 30 23:32:26 2024 +0200 +++ b/src/HOL/List.thy Tue Oct 01 20:39:16 2024 +0200 @@ -47,8 +47,6 @@ syntax "_list" :: "args => 'a list" (\(\indent=1 notation=\mixfix list enumeration\\[_])\) -syntax_consts - Cons translations "[x, xs]" == "x#[xs]" "[x]" == "x#[]" @@ -137,9 +135,6 @@ "_lupdbinds" :: "[lupdbind, lupdbinds] => lupdbinds" (\_,/ _\) "_LUpdate" :: "['a, lupdbinds] => 'a" (\_/[(_)]\ [1000,0] 900) -syntax_consts - list_update - translations "_LUpdate xs (_lupdbinds b bs)" == "_LUpdate (_LUpdate xs b) bs" "xs[i:=x]" == "CONST list_update xs i x" diff -r 843dba3d307a -r c007e6d9941d src/HOL/Metis_Examples/Message.thy --- a/src/HOL/Metis_Examples/Message.thy Mon Sep 30 23:32:26 2024 +0200 +++ b/src/HOL/Metis_Examples/Message.thy Tue Oct 01 20:39:16 2024 +0200 @@ -50,8 +50,6 @@ text\Concrete syntax: messages appear as \\A,B,NA\\, etc...\ syntax "_MTuple" :: "['a, args] \ 'a * 'b" (\(\indent=2 notation=\mixfix message tuple\\\_,/ _\)\) -syntax_consts - MPair translations "\x, y, z\" \ "\x, \y, z\\" "\x, y\" \ "CONST MPair x y" diff -r 843dba3d307a -r c007e6d9941d src/HOL/Product_Type.thy --- a/src/HOL/Product_Type.thy Mon Sep 30 23:32:26 2024 +0200 +++ b/src/HOL/Product_Type.thy Tue Oct 01 20:39:16 2024 +0200 @@ -294,7 +294,6 @@ "_patterns" :: "pttrn \ patterns \ patterns" (\_,/ _\) "_unit" :: pttrn (\'(')\) syntax_consts - Pair and "_pattern" "_patterns" \ case_prod and "_unit" \ case_unit translations diff -r 843dba3d307a -r c007e6d9941d src/HOL/Prolog/Test.thy --- a/src/HOL/Prolog/Test.thy Mon Sep 30 23:32:26 2024 +0200 +++ b/src/HOL/Prolog/Test.thy Tue Oct 01 20:39:16 2024 +0200 @@ -20,8 +20,6 @@ syntax "_list" :: "args => 'a list" (\(\indent=1 notation=\mixfix list enumeration\\[_])\) -syntax_consts - Cons translations "[x, xs]" == "x#[xs]" "[x]" == "x#[]" diff -r 843dba3d307a -r c007e6d9941d src/HOL/Quotient_Examples/Lift_FSet.thy --- a/src/HOL/Quotient_Examples/Lift_FSet.thy Mon Sep 30 23:32:26 2024 +0200 +++ b/src/HOL/Quotient_Examples/Lift_FSet.thy Tue Oct 01 20:39:16 2024 +0200 @@ -97,8 +97,6 @@ syntax "_fset" :: "args => 'a fset" (\(\indent=2 notation=\mixfix finite set enumeration\\{|_|})\) -syntax_consts - fcons translations "{|x, xs|}" == "CONST fcons x {|xs|}" "{|x|}" == "CONST fcons x {||}" diff -r 843dba3d307a -r c007e6d9941d src/HOL/Quotient_Examples/Quotient_FSet.thy --- a/src/HOL/Quotient_Examples/Quotient_FSet.thy Mon Sep 30 23:32:26 2024 +0200 +++ b/src/HOL/Quotient_Examples/Quotient_FSet.thy Tue Oct 01 20:39:16 2024 +0200 @@ -290,8 +290,6 @@ syntax "_fset" :: "args => 'a fset" (\(\indent=2 notation=\mixfix finite set enumeration\\{|_|})\) -syntax_consts - insert_fset translations "{|x, xs|}" == "CONST insert_fset x {|xs|}" "{|x|}" == "CONST insert_fset x {||}" diff -r 843dba3d307a -r c007e6d9941d src/HOL/SET_Protocol/Message_SET.thy --- a/src/HOL/SET_Protocol/Message_SET.thy Mon Sep 30 23:32:26 2024 +0200 +++ b/src/HOL/SET_Protocol/Message_SET.thy Tue Oct 01 20:39:16 2024 +0200 @@ -70,8 +70,6 @@ (*Concrete syntax: messages appear as \\A,B,NA\\, etc...*) syntax "_MTuple" :: "['a, args] \ 'a * 'b" (\(\indent=2 notation=\mixfix message tuple\\\_,/ _\)\) -syntax_consts - MPair translations "\x, y, z\" \ "\x, \y, z\\" "\x, y\" \ "CONST MPair x y" diff -r 843dba3d307a -r c007e6d9941d src/HOL/Set.thy --- a/src/HOL/Set.thy Mon Sep 30 23:32:26 2024 +0200 +++ b/src/HOL/Set.thy Tue Oct 01 20:39:16 2024 +0200 @@ -145,8 +145,6 @@ syntax "_Finset" :: "args \ 'a set" (\(\indent=1 notation=\mixfix set enumeration\\{_})\) -syntax_consts - insert translations "{x, xs}" \ "CONST insert x {xs}" "{x}" \ "CONST insert x {}" diff -r 843dba3d307a -r c007e6d9941d src/HOL/ex/Code_Lazy_Demo.thy --- a/src/HOL/ex/Code_Lazy_Demo.thy Mon Sep 30 23:32:26 2024 +0200 +++ b/src/HOL/ex/Code_Lazy_Demo.thy Tue Oct 01 20:39:16 2024 +0200 @@ -41,8 +41,6 @@ syntax "_llist" :: "args => 'a list" (\(\indent=1 notation=\mixfix lazy list enumeration\\\<^bold>\_\<^bold>\)\) -syntax_consts - LCons translations "\<^bold>\x, xs\<^bold>\" == "x###\<^bold>\xs\<^bold>\" "\<^bold>\x\<^bold>\" == "x###\<^bold>\\<^bold>\" diff -r 843dba3d307a -r c007e6d9941d src/ZF/Induct/Multiset.thy --- a/src/ZF/Induct/Multiset.thy Mon Sep 30 23:32:26 2024 +0200 +++ b/src/ZF/Induct/Multiset.thy Tue Oct 01 20:39:16 2024 +0200 @@ -75,8 +75,6 @@ syntax "_MColl" :: "[pttrn, i, o] \ i" (\(\indent=1 notation=\mixfix multiset comprehension\\{# _ \ _./ _#})\) -syntax_consts - MCollect translations "{#x \ M. P#}" == "CONST MCollect(M, \x. P)" diff -r 843dba3d307a -r c007e6d9941d src/ZF/List.thy --- a/src/ZF/List.thy Mon Sep 30 23:32:26 2024 +0200 +++ b/src/ZF/List.thy Tue Oct 01 20:39:16 2024 +0200 @@ -17,8 +17,6 @@ syntax "_List" :: "is \ i" (\(\indent=1 notation=\mixfix list enumeration\\[_])\) -syntax_consts - Cons translations "[x, xs]" == "CONST Cons(x, [xs])" "[x]" == "CONST Cons(x, [])" diff -r 843dba3d307a -r c007e6d9941d src/ZF/ZF_Base.thy --- a/src/ZF/ZF_Base.thy Mon Sep 30 23:32:26 2024 +0200 +++ b/src/ZF/ZF_Base.thy Tue Oct 01 20:39:16 2024 +0200 @@ -56,8 +56,6 @@ syntax "_Replace" :: "[pttrn, pttrn, i, o] \ i" (\(\indent=1 notation=\mixfix relational replacement\\{_ ./ _ \ _, _})\) -syntax_consts - Replace translations "{y. x\A, Q}" \ "CONST Replace(A, \x y. Q)" @@ -69,8 +67,6 @@ syntax "_RepFun" :: "[i, pttrn, i] \ i" (\(\indent=1 notation=\mixfix functional replacement\\{_ ./ _ \ _})\ [51,0,51]) -syntax_consts - RepFun translations "{b. x\A}" \ "CONST RepFun(A, \x. b)" @@ -81,8 +77,6 @@ syntax "_Collect" :: "[pttrn, i, o] \ i" (\(\indent=1 notation=\mixfix set comprehension\\{_ \ _ ./ _})\) -syntax_consts - Collect translations "{x\A. P}" \ "CONST Collect(A, \x. P)" @@ -134,8 +128,6 @@ "" :: "i \