--- a/src/HOL/Enum.thy Mon Jan 30 13:55:21 2012 +0100
+++ b/src/HOL/Enum.thy Mon Jan 30 13:55:22 2012 +0100
@@ -791,6 +791,10 @@
"tranclp r a b \<equiv> (a, b) \<in> trancl {(x, y). r x y}"
by (simp add: trancl_def)
+lemma rtranclp_rtrancl_eq[code, no_atp]:
+ "rtranclp r x y = ((x, y) : rtrancl {(x, y). r x y})"
+unfolding rtrancl_def by auto
+
lemma max_ext_eq[code]:
"max_ext R = {(X, Y). finite X & finite Y & Y ~={} & (ALL x. x : X --> (EX xa : Y. (x, xa) : R))}"
by (auto simp add: max_ext.simps)