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"