Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Transitive_Closure.thy
changeset 45137 6e422d180de8
parent 45116 f947eeef6b6f
child 45139 bdcaa3f3a2f4 
--- 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
isabelle