src/HOL/Enum.thy
changeset 46357 2795607a1f40
parent 46352 73b03235799a
child 46358 b2a936486685
equal deleted inserted replaced
46356:48fcca8965f4 46357:2795607a1f40
   785 
   785 
   786 lemma [code]:
   786 lemma [code]:
   787   "Collect P = set (filter P enum)"
   787   "Collect P = set (filter P enum)"
   788 by (auto simp add: enum_UNIV)
   788 by (auto simp add: enum_UNIV)
   789 
   789 
       
   790 lemma tranclp_unfold [code, no_atp]:
       
   791   "tranclp r a b \<equiv> (a, b) \<in> trancl {(x, y). r x y}"
       
   792 by (simp add: trancl_def)
   790 
   793 
   791 subsection {* Executable accessible part *}
   794 subsection {* Executable accessible part *}
   792 (* FIXME: should be moved somewhere else !? *)
   795 (* FIXME: should be moved somewhere else !? *)
   793 
   796 
   794 subsubsection {* Finite monotone eventually stable sequences *}
   797 subsubsection {* Finite monotone eventually stable sequences *}