src/HOL/Predicate.thy
changeset 31105 95f66b234086
parent 30430 42ea5d85edcc
child 31106 9a1178204dc0
--- a/src/HOL/Predicate.thy	Tue Apr 21 09:53:31 2009 +0200
+++ b/src/HOL/Predicate.thy	Wed Apr 22 11:10:23 2009 +0200
@@ -622,6 +622,11 @@
   "pred_rec f P = f (eval P)"
   by (cases P) simp
 
+inductive eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where "eq x x"
+
+lemma eq_is_eq: "eq x y \<equiv> (x = y)"
+by (rule eq_reflection) (auto intro: eq.intros elim: eq.cases)
+
 no_notation
   inf (infixl "\<sqinter>" 70) and
   sup (infixl "\<squnion>" 65) and
@@ -633,6 +638,6 @@
 
 hide (open) type pred seq
 hide (open) const Pred eval single bind if_pred not_pred
-  Empty Insert Join Seq member pred_of_seq "apply" adjunct
+  Empty Insert Join Seq member pred_of_seq "apply" adjunct eq
 
 end