src/HOL/Predicate.thy

--- a/src/HOL/Predicate.thy	Tue Mar 18 21:02:33 2014 +0100
+++ b/src/HOL/Predicate.thy	Tue Mar 18 22:11:46 2014 +0100
@@ -83,11 +83,11 @@
 
 end
 
-lemma eval_INFI [simp]:
+lemma eval_INF [simp]:
   "eval (INFI A f) = INFI A (eval \<circ> f)"
   using eval_Inf [of "f ` A"] by simp
 
-lemma eval_SUPR [simp]:
+lemma eval_SUP [simp]:
   "eval (SUPR A f) = SUPR A (eval \<circ> f)"
   using eval_Sup [of "f ` A"] by simp