# HG changeset patch
# User bulwahn
# Date 1327928121 -3600
# Node ID b2a93648668511dd64c2f8fcaa76b9c78c05759a
# Parent  2795607a1f4009d939631cb7c68f9f91dafade31
adding code equation for max_ext

diff -r 2795607a1f40 -r b2a936486685 src/HOL/Enum.thy
--- 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 !? *)