src/HOL/Library/RBT_Set.thy
changeset 56218 1c3f1f2431f9
parent 56212 3253aaf73a01
child 56519 c1048f5bbb45
--- a/src/HOL/Library/RBT_Set.thy	Wed Mar 19 17:06:02 2014 +0000
+++ b/src/HOL/Library/RBT_Set.thy	Wed Mar 19 18:47:22 2014 +0100
@@ -112,7 +112,7 @@
   "Inf_fin = Inf_fin" ..
 
 lemma [code, code del]:
-  "INFI = INFI" ..
+  "INFIMUM = INFIMUM" ..
 
 lemma [code, code del]:
   "Max = Max" ..
@@ -121,7 +121,7 @@
   "Sup_fin = Sup_fin" ..
 
 lemma [code, code del]:
-  "SUPR = SUPR" ..
+  "SUPREMUM = SUPREMUM" ..
 
 lemma [code, code del]:
   "(Inf :: 'a set set \<Rightarrow> 'a set) = Inf" ..
@@ -759,7 +759,7 @@
 
 lemma INF_Set_fold [code]:
   fixes f :: "_ \<Rightarrow> 'a::complete_lattice"
-  shows "INFI (Set t) f = fold_keys (inf \<circ> f) t top"
+  shows "INFIMUM (Set t) f = fold_keys (inf \<circ> f) t top"
 proof -
   have "comp_fun_commute ((inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a) \<circ> f)" 
     by default (auto simp add: fun_eq_iff ac_simps)
@@ -800,7 +800,7 @@
 
 lemma SUP_Set_fold [code]:
   fixes f :: "_ \<Rightarrow> 'a::complete_lattice"
-  shows "SUPR (Set t) f = fold_keys (sup \<circ> f) t bot"
+  shows "SUPREMUM (Set t) f = fold_keys (sup \<circ> f) t bot"
 proof -
   have "comp_fun_commute ((sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a) \<circ> f)" 
     by default (auto simp add: fun_eq_iff ac_simps)