# HG changeset patch
# User haftmann
# Date 1236587679 -3600
# Node ID e0247e990702f20784cb8b6dae46b5b832d356f0
# Parent  26a05c2fd577d28a614b52da51920ae5db36bd3e
dropped eq_pred

diff -r 26a05c2fd577 -r e0247e990702 src/HOL/Predicate.thy
--- a/src/HOL/Predicate.thy	Sun Mar 08 17:25:16 2009 +0100
+++ b/src/HOL/Predicate.thy	Mon Mar 09 09:34:39 2009 +0100
@@ -470,9 +470,6 @@
 definition if_pred :: "bool \<Rightarrow> unit pred" where
   if_pred_eq: "if_pred b = (if b then single () else \<bottom>)"
 
-definition eq_pred :: "'a \<Rightarrow> 'a \<Rightarrow> unit pred" where
-  eq_pred_eq: "eq_pred a b = if_pred (a = b)"
-
 definition not_pred :: "unit pred \<Rightarrow> unit pred" where
   not_pred_eq: "not_pred P = (if eval P () then \<bottom> else single ())"
 
@@ -482,12 +479,6 @@
 lemma if_predE: "eval (if_pred b) x \<Longrightarrow> (b \<Longrightarrow> x = () \<Longrightarrow> P) \<Longrightarrow> P"
   unfolding if_pred_eq by (cases b) (auto elim: botE)
 
-lemma eq_predI: "eval (eq_pred a a) ()"
-  unfolding eq_pred_eq if_pred_eq by (auto intro: singleI)
-
-lemma eq_predE: "eval (eq_pred a b) x \<Longrightarrow> (a = b \<Longrightarrow> x = () \<Longrightarrow> P) \<Longrightarrow> P"
-  unfolding eq_pred_eq by (erule if_predE)
-
 lemma not_predI: "\<not> P \<Longrightarrow> eval (not_pred (Pred (\<lambda>u. P))) ()"
   unfolding not_pred_eq eval_pred by (auto intro: singleI)
 
@@ -609,7 +600,7 @@
   bind (infixl "\<guillemotright>=" 70)
 
 hide (open) type pred seq
-hide (open) const Pred eval single bind if_pred eq_pred not_pred
+hide (open) const Pred eval single bind if_pred not_pred
   Empty Insert Join Seq member "apply" adjunct
 
 end