1.1 --- a/src/HOL/Predicate.thy	Tue Apr 21 09:53:31 2009 +0200
     1.2 +++ b/src/HOL/Predicate.thy	Wed Apr 22 11:10:23 2009 +0200
     1.3 @@ -622,6 +622,11 @@
     1.4    "pred_rec f P = f (eval P)"
     1.5    by (cases P) simp
     1.6  
     1.7 +inductive eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where "eq x x"
     1.8 +
     1.9 +lemma eq_is_eq: "eq x y \<equiv> (x = y)"
    1.10 +by (rule eq_reflection) (auto intro: eq.intros elim: eq.cases)
    1.11 +
    1.12  no_notation
    1.13    inf (infixl "\<sqinter>" 70) and
    1.14    sup (infixl "\<squnion>" 65) and
    1.15 @@ -633,6 +638,6 @@
    1.16  
    1.17  hide (open) type pred seq
    1.18  hide (open) const Pred eval single bind if_pred not_pred
    1.19 -  Empty Insert Join Seq member pred_of_seq "apply" adjunct
    1.20 +  Empty Insert Join Seq member pred_of_seq "apply" adjunct eq
    1.21  
    1.22  end