equal
deleted
inserted
replaced
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 Relation |
9 imports Relation |
10 uses "~~/src/Provers/trancl.ML" |
|
11 begin |
10 begin |
|
11 |
|
12 ML_file "~~/src/Provers/trancl.ML" |
12 |
13 |
13 text {* |
14 text {* |
14 @{text rtrancl} is reflexive/transitive closure, |
15 @{text rtrancl} is reflexive/transitive closure, |
15 @{text trancl} is transitive closure, |
16 @{text trancl} is transitive closure, |
16 @{text reflcl} is reflexive closure. |
17 @{text reflcl} is reflexive closure. |