diff -r dd58f13a8eb4 -r eb85850d3eb7 src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Fri Nov 17 02:19:55 2006 +0100
+++ b/src/HOL/Transitive_Closure.thy	Fri Nov 17 02:20:03 2006 +0100
@@ -37,17 +37,17 @@
     trancl_into_trancl [Pure.intro]: "(a, b) : r^+ ==> (b, c) : r ==> (a,c) : r^+"
 
 abbreviation
-  reflcl :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_^=)" [1000] 999)
+  reflcl :: "('a \<times> 'a) set => ('a \<times> 'a) set"  ("(_^=)" [1000] 999) where
   "r^= == r \<union> Id"
 
 notation (xsymbols)
-  rtrancl  ("(_\<^sup>*)" [1000] 999)
-  trancl  ("(_\<^sup>+)" [1000] 999)
+  rtrancl  ("(_\<^sup>*)" [1000] 999) and
+  trancl  ("(_\<^sup>+)" [1000] 999) and
   reflcl  ("(_\<^sup>=)" [1000] 999)
 
 notation (HTML output)
-  rtrancl  ("(_\<^sup>*)" [1000] 999)
-  trancl  ("(_\<^sup>+)" [1000] 999)
+  rtrancl  ("(_\<^sup>*)" [1000] 999) and
+  trancl  ("(_\<^sup>+)" [1000] 999) and
   reflcl  ("(_\<^sup>=)" [1000] 999)