author | nipkow |
Sun, 30 Sep 2018 07:46:38 +0200 | |
changeset 69084 | c7c38c901267 |
parent 69083 | 6f8ae6ddc26b |
child 69085 | 9999d7823b8f |
src/HOL/List.thy | file | annotate | diff | comparison | revisions |
--- a/src/HOL/List.thy Sat Sep 29 23:23:43 2018 +0200 +++ b/src/HOL/List.thy Sun Sep 30 07:46:38 2018 +0200 @@ -130,7 +130,7 @@ "_lupdbind":: "['a, 'a] => lupdbind" ("(2_ :=/ _)") "" :: "lupdbind => lupdbinds" ("_") "_lupdbinds" :: "[lupdbind, lupdbinds] => lupdbinds" ("_,/ _") - "_LUpdate" :: "['a, lupdbinds] => 'a" ("_/[(_)]" [900,0] 900) + "_LUpdate" :: "['a, lupdbinds] => 'a" ("_/[(_)]" [1000,0] 900) translations "_LUpdate xs (_lupdbinds b bs)" == "_LUpdate (_LUpdate xs b) bs"