src/HOL/Library/RBT_Set.thy
changeset 56218 1c3f1f2431f9
parent 56212 3253aaf73a01
child 56519 c1048f5bbb45
     1.1 --- a/src/HOL/Library/RBT_Set.thy	Wed Mar 19 17:06:02 2014 +0000
     1.2 +++ b/src/HOL/Library/RBT_Set.thy	Wed Mar 19 18:47:22 2014 +0100
     1.3 @@ -112,7 +112,7 @@
     1.4    "Inf_fin = Inf_fin" ..
     1.5  
     1.6  lemma [code, code del]:
     1.7 -  "INFI = INFI" ..
     1.8 +  "INFIMUM = INFIMUM" ..
     1.9  
    1.10  lemma [code, code del]:
    1.11    "Max = Max" ..
    1.12 @@ -121,7 +121,7 @@
    1.13    "Sup_fin = Sup_fin" ..
    1.14  
    1.15  lemma [code, code del]:
    1.16 -  "SUPR = SUPR" ..
    1.17 +  "SUPREMUM = SUPREMUM" ..
    1.18  
    1.19  lemma [code, code del]:
    1.20    "(Inf :: 'a set set \<Rightarrow> 'a set) = Inf" ..
    1.21 @@ -759,7 +759,7 @@
    1.22  
    1.23  lemma INF_Set_fold [code]:
    1.24    fixes f :: "_ \<Rightarrow> 'a::complete_lattice"
    1.25 -  shows "INFI (Set t) f = fold_keys (inf \<circ> f) t top"
    1.26 +  shows "INFIMUM (Set t) f = fold_keys (inf \<circ> f) t top"
    1.27  proof -
    1.28    have "comp_fun_commute ((inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a) \<circ> f)" 
    1.29      by default (auto simp add: fun_eq_iff ac_simps)
    1.30 @@ -800,7 +800,7 @@
    1.31  
    1.32  lemma SUP_Set_fold [code]:
    1.33    fixes f :: "_ \<Rightarrow> 'a::complete_lattice"
    1.34 -  shows "SUPR (Set t) f = fold_keys (sup \<circ> f) t bot"
    1.35 +  shows "SUPREMUM (Set t) f = fold_keys (sup \<circ> f) t bot"
    1.36  proof -
    1.37    have "comp_fun_commute ((sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a) \<circ> f)" 
    1.38      by default (auto simp add: fun_eq_iff ac_simps)