src/HOL/Enum.thy
changeset 46357 2795607a1f40
parent 46352 73b03235799a
child 46358 b2a936486685
     1.1 --- a/src/HOL/Enum.thy	Mon Jan 30 13:55:19 2012 +0100
     1.2 +++ b/src/HOL/Enum.thy	Mon Jan 30 13:55:20 2012 +0100
     1.3 @@ -787,6 +787,9 @@
     1.4    "Collect P = set (filter P enum)"
     1.5  by (auto simp add: enum_UNIV)
     1.6  
     1.7 +lemma tranclp_unfold [code, no_atp]:
     1.8 +  "tranclp r a b \<equiv> (a, b) \<in> trancl {(x, y). r x y}"
     1.9 +by (simp add: trancl_def)
    1.10  
    1.11  subsection {* Executable accessible part *}
    1.12  (* FIXME: should be moved somewhere else !? *)