summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Enum.thy

changeset 45119 | 055c6ff9c5c3 |

parent 45117 | 3911cf09899a |

child 45140 | 339a8b3c4791 |

1.1 --- a/src/HOL/Enum.thy Mon Oct 03 14:43:15 2011 +0200 1.2 +++ b/src/HOL/Enum.thy Mon Oct 03 15:39:30 2011 +0200 1.3 @@ -766,7 +766,7 @@ 1.4 1.5 subsection {* An executable (reflexive) transitive closure on finite relations *} 1.6 1.7 -text {* Definitions could be moved to Transitive_Closure if they are of more general use. *} 1.8 +text {* Definitions could be moved to Transitive Closure theory if they are of more general use. *} 1.9 1.10 definition ntrancl :: "('a * 'a => bool) => nat => ('a * 'a => bool)" 1.11 where