# HG changeset patch # User wenzelm # Date 1727694042 -7200 # Node ID 83596aea48cb59a88a6903e6f7ccd4264862c7bf # Parent bc5eb7841b74acde457cf37de38e021c820e7d4e less markup: prefer "notatation" over "entity"; diff -r bc5eb7841b74 -r 83596aea48cb src/HOL/Fun.thy --- a/src/HOL/Fun.thy Mon Sep 30 12:59:50 2024 +0200 +++ b/src/HOL/Fun.thy Mon Sep 30 13:00:42 2024 +0200 @@ -844,10 +844,10 @@ "_updbind" :: "'a \ 'a \ updbind" (\(\indent=2 notation=\mixfix update\\_ :=/ _)\) "" :: "updbind \ updbinds" (\_\) "_updbinds":: "updbind \ updbinds \ updbinds" (\_,/ _\) - "_Update" :: "'a \ updbinds \ 'a" (\_/'((\indent=2 notation=\mixfix updates\\_)')\ [1000, 0] 900) + "_Update" :: "'a \ updbinds \ 'a" (\_/'((2_)')\ [1000, 0] 900) syntax_consts - "_updbind" "_updbinds" "_Update" \ fun_upd + fun_upd translations "_Update f (_updbinds b bs)" \ "_Update (_Update f b) bs" diff -r bc5eb7841b74 -r 83596aea48cb src/HOL/List.thy --- a/src/HOL/List.thy Mon Sep 30 12:59:50 2024 +0200 +++ b/src/HOL/List.thy Mon Sep 30 13:00:42 2024 +0200 @@ -141,7 +141,7 @@ "_LUpdate" :: "['a, lupdbinds] => 'a" (\_/[(_)]\ [1000,0] 900) syntax_consts - "_lupdbind" "_lupdbinds" "_LUpdate" == list_update + list_update translations "_LUpdate xs (_lupdbinds b bs)" == "_LUpdate (_LUpdate xs b) bs" diff -r bc5eb7841b74 -r 83596aea48cb src/HOL/Product_Type.thy --- a/src/HOL/Product_Type.thy Mon Sep 30 12:59:50 2024 +0200 +++ b/src/HOL/Product_Type.thy Mon Sep 30 13:00:42 2024 +0200 @@ -294,7 +294,7 @@ "_patterns" :: "pttrn \ patterns \ patterns" (\_,/ _\) "_unit" :: pttrn (\'(')\) syntax_consts - "_tuple" "_tuple_arg" "_tuple_args" \ Pair and + Pair and "_pattern" "_patterns" \ case_prod and "_unit" \ case_unit translations