more abbrevs;
authorwenzelm
Sun, 25 Feb 2018 19:19:11 +0100
changeset 67723 d11c5af083a5
parent 67722 012f1e8a1209
child 67724 63e305429f8a
more abbrevs;
src/HOL/Transitive_Closure.thy
--- 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"