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