# HG changeset patch
# User krauss
# Date 1159284784 -7200
# Node ID a6686a8e1b687a5cb2ebb6774114cb35df3a14ee
# Parent  c1f16b427d86d8c0776c4d586300f5348db71b9e
Changed precedence of "op O" (relation composition) from 60 to 75.

diff -r c1f16b427d86 -r a6686a8e1b68 NEWS
--- a/NEWS	Tue Sep 26 13:34:35 2006 +0200
+++ b/NEWS	Tue Sep 26 17:33:04 2006 +0200
@@ -534,6 +534,9 @@
 
 * "LEAST x:A. P" expands to "LEAST x. x:A & P" (input only).
 
+* Relation composition operator "op O" now has precedence 75 and binds
+stronger than union and intersection. INCOMPATIBILITY.
+
 * The old set interval syntax "{m..n(}" (and relatives) has been removed.
   Use "{m..<n}" (and relatives) instead.
 
diff -r c1f16b427d86 -r a6686a8e1b68 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Tue Sep 26 13:34:35 2006 +0200
+++ b/src/HOL/Relation.thy	Tue Sep 26 17:33:04 2006 +0200
@@ -20,7 +20,7 @@
   converse  ("(_\<inverse>)" [1000] 999)
 
 definition
-  rel_comp  :: "[('b * 'c) set, ('a * 'b) set] => ('a * 'c) set"  (infixr "O" 60)
+  rel_comp  :: "[('b * 'c) set, ('a * 'b) set] => ('a * 'c) set"  (infixr "O" 75)
   "r O s == {(x,z). EX y. (x, y) : s & (y, z) : r}"
 
   Image :: "[('a * 'b) set, 'a set] => 'b set"                (infixl "``" 90)
diff -r c1f16b427d86 -r a6686a8e1b68 src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Tue Sep 26 13:34:35 2006 +0200
+++ b/src/HOL/Transitive_Closure.thy	Tue Sep 26 17:33:04 2006 +0200
@@ -208,7 +208,7 @@
   by (blast elim: rtranclE converse_rtranclE
     intro: rtrancl_into_rtrancl converse_rtrancl_into_rtrancl)
 
-lemma rtrancl_unfold: "r^* = Id Un (r O r^*)"
+lemma rtrancl_unfold: "r^* = Id Un r O r^*"
   by (auto intro: rtrancl_into_rtrancl elim: rtranclE)
 
 
@@ -263,7 +263,7 @@
 
 inductive_cases tranclE: "(a, b) : r^+"
 
-lemma trancl_unfold: "r^+ = r Un (r O r^+)"
+lemma trancl_unfold: "r^+ = r Un r O r^+"
   by (auto intro: trancl_into_trancl elim: tranclE)
 
 lemma trans_trancl[simp]: "trans(r^+)"