author | bulwahn |
Mon, 03 Oct 2011 15:39:30 +0200 | |
changeset 45119 | 055c6ff9c5c3 |
parent 45118 | 7462f287189a |
child 45120 | 717bc892e4d7 |
src/HOL/Enum.thy | file | annotate | diff | comparison | revisions |
--- a/src/HOL/Enum.thy Mon Oct 03 14:43:15 2011 +0200 +++ b/src/HOL/Enum.thy Mon Oct 03 15:39:30 2011 +0200 @@ -766,7 +766,7 @@ subsection {* An executable (reflexive) transitive closure on finite relations *} -text {* Definitions could be moved to Transitive_Closure if they are of more general use. *} +text {* Definitions could be moved to Transitive Closure theory if they are of more general use. *} definition ntrancl :: "('a * 'a => bool) => nat => ('a * 'a => bool)" where