--- a/src/HOL/Induct/Com.thy Wed May 07 10:56:58 2008 +0200
+++ b/src/HOL/Induct/Com.thy Wed May 07 10:57:19 2008 +0200
@@ -85,11 +85,11 @@
lemma [pred_set_conv]:
"((\<lambda>x x' y y'. ((x, x'), (y, y')) \<in> R) <= (\<lambda>x x' y y'. ((x, x'), (y, y')) \<in> S)) = (R <= S)"
- by (auto simp add: le_fun_def le_bool_def)
+ by (auto simp add: le_fun_def le_bool_def mem_def)
lemma [pred_set_conv]:
"((\<lambda>x x' y. ((x, x'), y) \<in> R) <= (\<lambda>x x' y. ((x, x'), y) \<in> S)) = (R <= S)"
- by (auto simp add: le_fun_def le_bool_def)
+ by (auto simp add: le_fun_def le_bool_def mem_def)
declare [[unify_trace_bound = 30, unify_search_bound = 60]]