--- a/src/HOL/Transitive_Closure.thy Thu Oct 13 22:50:35 2011 +0200
+++ b/src/HOL/Transitive_Closure.thy Thu Oct 13 22:56:19 2011 +0200
@@ -44,11 +44,11 @@
abbreviation
reflclp :: "('a => 'a => bool) => 'a => 'a => bool" ("(_^==)" [1000] 1000) where
- "r^== == sup r op ="
+ "r^== \<equiv> sup r op ="
abbreviation
reflcl :: "('a \<times> 'a) set => ('a \<times> 'a) set" ("(_^=)" [1000] 999) where
- "r^= == r \<union> Id"
+ "r^= \<equiv> r \<union> Id"
notation (xsymbols)
rtranclp ("(_\<^sup>*\<^sup>*)" [1000] 1000) and