changeset 77695 | 93531ba2c784 |
parent 76751 | 66f17783913b |
child 79611 | 97612262718a |
--- a/src/HOL/Transitive_Closure.thy Mon Mar 20 11:13:01 2023 +0100 +++ b/src/HOL/Transitive_Closure.thy Mon Mar 20 15:01:12 2023 +0100 @@ -6,7 +6,7 @@ section \<open>Reflexive and Transitive closure of a relation\<close> theory Transitive_Closure - imports Relation + imports Finite_Set abbrevs "^*" = "\<^sup>*" "\<^sup>*\<^sup>*" and "^+" = "\<^sup>+" "\<^sup>+\<^sup>+" and "^=" = "\<^sup>=" "\<^sup>=\<^sup>="