changeset 46635 | cde737f9c911 |
parent 46362 | b2878f059f91 |
child 46638 | fc315796794e |
46634:c6d2fc7095ac | 46635:cde737f9c911 |
---|---|
4 *) |
4 *) |
5 |
5 |
6 header {* Reflexive and Transitive closure of a relation *} |
6 header {* Reflexive and Transitive closure of a relation *} |
7 |
7 |
8 theory Transitive_Closure |
8 theory Transitive_Closure |
9 imports Predicate |
9 imports Relation |
10 uses "~~/src/Provers/trancl.ML" |
10 uses "~~/src/Provers/trancl.ML" |
11 begin |
11 begin |
12 |
12 |
13 text {* |
13 text {* |
14 @{text rtrancl} is reflexive/transitive closure, |
14 @{text rtrancl} is reflexive/transitive closure, |