equal
deleted
inserted
replaced
5 |
5 |
6 section \<open>Reflexive and Transitive closure of a relation\<close> |
6 section \<open>Reflexive and Transitive closure of a relation\<close> |
7 |
7 |
8 theory Transitive_Closure |
8 theory Transitive_Closure |
9 imports Relation |
9 imports Relation |
|
10 abbrevs "^*" = "\<^sup>*" "\<^sup>*\<^sup>*" |
|
11 and "^+" = "\<^sup>+" "\<^sup>+\<^sup>+" |
|
12 and "^=" = "\<^sup>=" "\<^sup>=\<^sup>=" |
10 begin |
13 begin |
11 |
14 |
12 ML_file "~~/src/Provers/trancl.ML" |
15 ML_file "~~/src/Provers/trancl.ML" |
13 |
16 |
14 text \<open> |
17 text \<open> |