equal
deleted
inserted
replaced
4 Copyright 1992 University of Cambridge |
4 Copyright 1992 University of Cambridge |
5 *) |
5 *) |
6 |
6 |
7 header {* Reflexive and Transitive closure of a relation *} |
7 header {* Reflexive and Transitive closure of a relation *} |
8 |
8 |
9 theory Transitive_Closure = Inductive |
9 theory Transitive_Closure |
10 |
10 import Inductive |
11 files ("../Provers/trancl.ML"): |
11 files ("../Provers/trancl.ML") |
|
12 begin |
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. |