merged
authornipkow
Wed Nov 08 21:02:05 2017 +0100 (17 months ago)
changeset 67037a76fb0f4b9ca
parent 67035 8b7233175199
parent 67036 783c901a62cb
child 67038 db3e2240f830
merged
     1.1 --- a/src/HOL/Lattices_Big.thy	Wed Nov 08 17:36:21 2017 +0100
     1.2 +++ b/src/HOL/Lattices_Big.thy	Wed Nov 08 21:02:05 2017 +0100
     1.3 @@ -837,7 +837,7 @@
     1.4  
     1.5  syntax
     1.6    "_arg_min" :: "('a \<Rightarrow> 'b) \<Rightarrow> pttrn \<Rightarrow> bool \<Rightarrow> 'a"
     1.7 -    ("(3ARG'_MIN _ _./ _)" [0, 0, 10] 10)
     1.8 +    ("(3ARG'_MIN _ _./ _)" [1000, 0, 10] 10)
     1.9  translations
    1.10    "ARG_MIN f x. P" \<rightleftharpoons> "CONST arg_min f (\<lambda>x. P)"
    1.11  
    1.12 @@ -945,7 +945,7 @@
    1.13  
    1.14  syntax
    1.15    "_arg_max" :: "('a \<Rightarrow> 'b) \<Rightarrow> pttrn \<Rightarrow> bool \<Rightarrow> 'a"
    1.16 -    ("(3ARG'_MAX _ _./ _)" [0, 0, 10] 10)
    1.17 +    ("(3ARG'_MAX _ _./ _)" [1000, 0, 10] 10)
    1.18  translations
    1.19    "ARG_MAX f x. P" \<rightleftharpoons> "CONST arg_max f (\<lambda>x. P)"
    1.20