# HG changeset patch
# User berghofe
# Date 1184144591 -7200
# Node ID c5ead5df7f358df28a3649781840fbeb0a8163cb
# Parent  3a801ffdc58c2d2a58fc3c7bb2c14e365c362ebc
Inserted definition of in_rel again (since member2 was removed).

diff -r 3a801ffdc58c -r c5ead5df7f35 src/HOL/FunDef.thy
--- a/src/HOL/FunDef.thy	Wed Jul 11 11:02:07 2007 +0200
+++ b/src/HOL/FunDef.thy	Wed Jul 11 11:03:11 2007 +0200
@@ -85,6 +85,14 @@
     by (rule THE_default_none)
 qed
 
+definition in_rel_def[simp]:
+  "in_rel R x y == (x, y) \<in> R"
+
+lemma wf_in_rel:
+  "wf R \<Longrightarrow> wfP (in_rel R)"
+  by (simp add: wfP_def)
+
+
 use "Tools/function_package/fundef_lib.ML"
 use "Tools/function_package/fundef_common.ML"
 use "Tools/function_package/inductive_wrap.ML"