# HG changeset patch
# User wenzelm
# Date 1519582751 -3600
# Node ID d11c5af083a5fa314f446be9678bea45b3f8969c
# Parent  012f1e8a12095e7969dceb8d5fb12e63d13e095c
more abbrevs;

diff -r 012f1e8a1209 -r d11c5af083a5 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"