src/HOL/Predicate.thy

 lemma eval_minus [simp]:
   "eval (P - Q) = eval P - eval Q"
   by (simp add: minus_pred_def)
 
 instance proof
-qed (auto intro!: pred_eqI simp add: uminus_apply minus_apply INF_apply SUP_apply)
+qed (auto intro!: pred_eqI)
 
 end
 
 definition single :: "'a \<Rightarrow> 'a pred" where
   "single x = Pred ((op =) x)"

   "eval (P \<guillemotright>= f) = eval (SUPR {x. eval P x} f)"
   by (simp add: bind_def)
 
 lemma bind_bind:
   "(P \<guillemotright>= Q) \<guillemotright>= R = P \<guillemotright>= (\<lambda>x. Q x \<guillemotright>= R)"
-  by (rule pred_eqI) (auto simp add: SUP_apply)
+  by (rule pred_eqI) auto
 
 lemma bind_single:
   "P \<guillemotright>= single = P"
   by (rule pred_eqI) auto
 

   "(P \<squnion> Q) \<guillemotright>= R = P \<guillemotright>= R \<squnion> Q \<guillemotright>= R"
   by (rule pred_eqI) auto
 
 lemma Sup_bind:
   "(\<Squnion>A \<guillemotright>= f) = \<Squnion>((\<lambda>x. x \<guillemotright>= f) ` A)"
-  by (rule pred_eqI) (auto simp add: SUP_apply)
+  by (rule pred_eqI) auto
 
 lemma pred_iffI:
   assumes "\<And>x. eval A x \<Longrightarrow> eval B x"
   and "\<And>x. eval B x \<Longrightarrow> eval A x"
   shows "A = B"