author | wenzelm |
Sun, 25 Feb 2018 19:19:11 +0100 | |
changeset 67723 | d11c5af083a5 |
parent 67722 | 012f1e8a1209 |
child 67724 | 63e305429f8a |
--- a/src/HOL/Transitive_Closure.thy Sun Feb 25 19:16:32 2018 +0100 +++ b/src/HOL/Transitive_Closure.thy Sun Feb 25 19:19:11 2018 +0100 @@ -7,6 +7,9 @@ theory Transitive_Closure imports Relation + abbrevs "^*" = "\<^sup>*" "\<^sup>*\<^sup>*" + and "^+" = "\<^sup>+" "\<^sup>+\<^sup>+" + and "^=" = "\<^sup>=" "\<^sup>=\<^sup>=" begin ML_file "~~/src/Provers/trancl.ML"