# HG changeset patch
# User nipkow
# Date 1515227997 -3600
# Node ID f0f13aa282f49a9a90d051570d6484783dd402bf
# Parent  7905adb28bdcf0fd31e70d9e4b8a99b87b1bacb2
tuned op

diff -r 7905adb28bdc -r f0f13aa282f4 src/HOL/Algebra/Divisibility.thy
--- a/src/HOL/Algebra/Divisibility.thy	Fri Jan 05 19:32:56 2018 +0100
+++ b/src/HOL/Algebra/Divisibility.thy	Sat Jan 06 09:39:57 2018 +0100
@@ -145,7 +145,7 @@
 definition associated :: "[_, 'a, 'a] \<Rightarrow> bool" (infix "\<sim>\<index>" 55)
   where "a \<sim>\<^bsub>G\<^esub> b \<longleftrightarrow> a divides\<^bsub>G\<^esub> b \<and> b divides\<^bsub>G\<^esub> a"
 
-abbreviation "division_rel G \<equiv> \<lparr>carrier = carrier G, eq = op \<sim>\<^bsub>G\<^esub>, le = op divides\<^bsub>G\<^esub>\<rparr>"
+abbreviation "division_rel G \<equiv> \<lparr>carrier = carrier G, eq = op \<sim>\<^bsub>G\<^esub>, le = (op divides\<^bsub>G\<^esub>)\<rparr>"
 
 definition properfactor :: "[_, 'a, 'a] \<Rightarrow> bool"
   where "properfactor G a b \<longleftrightarrow> a divides\<^bsub>G\<^esub> b \<and> \<not>(b divides\<^bsub>G\<^esub> a)"