diff -r dc429a5b13c4 -r 1c3f1f2431f9 src/HOL/Predicate.thy
--- a/src/HOL/Predicate.thy	Wed Mar 19 17:06:02 2014 +0000
+++ b/src/HOL/Predicate.thy	Wed Mar 19 18:47:22 2014 +0100
@@ -65,17 +65,17 @@
   by (simp add: sup_pred_def)
 
 definition
-  "\<Sqinter>A = Pred (INFI A eval)"
+  "\<Sqinter>A = Pred (INFIMUM A eval)"
 
 lemma eval_Inf [simp]:
-  "eval (\<Sqinter>A) = INFI A eval"
+  "eval (\<Sqinter>A) = INFIMUM A eval"
   by (simp add: Inf_pred_def)
 
 definition
-  "\<Squnion>A = Pred (SUPR A eval)"
+  "\<Squnion>A = Pred (SUPREMUM A eval)"
 
 lemma eval_Sup [simp]:
-  "eval (\<Squnion>A) = SUPR A eval"
+  "eval (\<Squnion>A) = SUPREMUM A eval"
   by (simp add: Sup_pred_def)
 
 instance proof
@@ -84,11 +84,11 @@
 end
 
 lemma eval_INF [simp]:
-  "eval (INFI A f) = INFI A (eval \<circ> f)"
+  "eval (INFIMUM A f) = INFIMUM A (eval \<circ> f)"
   using eval_Inf [of "f ` A"] by simp
 
 lemma eval_SUP [simp]:
-  "eval (SUPR A f) = SUPR A (eval \<circ> f)"
+  "eval (SUPREMUM A f) = SUPREMUM A (eval \<circ> f)"
   using eval_Sup [of "f ` A"] by simp
 
 instantiation pred :: (type) complete_boolean_algebra
@@ -121,10 +121,10 @@
   by (simp add: single_def)
 
 definition bind :: "'a pred \<Rightarrow> ('a \<Rightarrow> 'b pred) \<Rightarrow> 'b pred" (infixl "\<guillemotright>=" 70) where
-  "P \<guillemotright>= f = (SUPR {x. eval P x} f)"
+  "P \<guillemotright>= f = (SUPREMUM {x. eval P x} f)"
 
 lemma eval_bind [simp]:
-  "eval (P \<guillemotright>= f) = eval (SUPR {x. eval P x} f)"
+  "eval (P \<guillemotright>= f) = eval (SUPREMUM {x. eval P x} f)"
   by (simp add: bind_def)
 
 lemma bind_bind: