src/HOL/Library/RBT_Set.thy
changeset 56212 3253aaf73a01
parent 56019 682bba24e474
child 56218 1c3f1f2431f9
--- a/src/HOL/Library/RBT_Set.thy	Tue Mar 18 21:02:33 2014 +0100
+++ b/src/HOL/Library/RBT_Set.thy	Tue Mar 18 22:11:46 2014 +0100
@@ -757,7 +757,7 @@
 declare Inf'_def[symmetric, code_unfold]
 declare Inf_Set_fold[folded Inf'_def, code]
 
-lemma INFI_Set_fold [code]:
+lemma INF_Set_fold [code]:
   fixes f :: "_ \<Rightarrow> 'a::complete_lattice"
   shows "INFI (Set t) f = fold_keys (inf \<circ> f) t top"
 proof -
@@ -798,7 +798,7 @@
 declare Sup'_def[symmetric, code_unfold]
 declare Sup_Set_fold[folded Sup'_def, code]
 
-lemma SUPR_Set_fold [code]:
+lemma SUP_Set_fold [code]:
   fixes f :: "_ \<Rightarrow> 'a::complete_lattice"
   shows "SUPR (Set t) f = fold_keys (sup \<circ> f) t bot"
 proof -