author | bulwahn |
Mon, 30 Jan 2012 13:55:21 +0100 | |
changeset 46358 | b2a936486685 |
parent 46357 | 2795607a1f40 |
child 46359 | 9bc43dc49d0a |
src/HOL/Enum.thy | file | annotate | diff | comparison | revisions |
--- a/src/HOL/Enum.thy Mon Jan 30 13:55:20 2012 +0100 +++ b/src/HOL/Enum.thy Mon Jan 30 13:55:21 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 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) + subsection {* Executable accessible part *} (* FIXME: should be moved somewhere else !? *)