src/HOL/Library/Disjoint_Sets.thy
changeset 67399 eab6ce8368fa
parent 63928 d81fb5b46a5c
child 68406 6beb45f6cf67
--- a/src/HOL/Library/Disjoint_Sets.thy	Wed Jan 10 15:21:49 2018 +0100
+++ b/src/HOL/Library/Disjoint_Sets.thy	Wed Jan 10 15:25:09 2018 +0100
@@ -38,7 +38,7 @@
   "disjoint A \<Longrightarrow> a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<noteq> b \<Longrightarrow> a \<inter> b = {}"
   unfolding disjoint_def by auto
 
-lemma disjoint_image: "inj_on f (\<Union>A) \<Longrightarrow> disjoint A \<Longrightarrow> disjoint (op ` f ` A)"
+lemma disjoint_image: "inj_on f (\<Union>A) \<Longrightarrow> disjoint A \<Longrightarrow> disjoint ((`) f ` A)"
   unfolding inj_on_def disjoint_def by blast
 
 lemma assumes "disjoint (A \<union> B)"
@@ -276,15 +276,15 @@
     by (auto simp add: partition_on_def pairwise_def intro!: F_disjnt)
 qed
 
-lemma partition_on_restrict: "partition_on A P \<Longrightarrow> partition_on (B \<inter> A) (op \<inter> B ` P - {{}})"
+lemma partition_on_restrict: "partition_on A P \<Longrightarrow> partition_on (B \<inter> A) ((\<inter>) B ` P - {{}})"
   by (intro partition_on_transform) (auto simp: disjnt_def)
 
-lemma partition_on_vimage: "partition_on A P \<Longrightarrow> partition_on (f -` A) (op -` f ` P - {{}})"
+lemma partition_on_vimage: "partition_on A P \<Longrightarrow> partition_on (f -` A) ((-`) f ` P - {{}})"
   by (intro partition_on_transform) (auto simp: disjnt_def)
 
 lemma partition_on_inj_image:
   assumes P: "partition_on A P" and f: "inj_on f A"
-  shows "partition_on (f ` A) (op ` f ` P - {{}})"
+  shows "partition_on (f ` A) ((`) f ` P - {{}})"
 proof (rule partition_on_transform[OF P])
   show "p \<in> P \<Longrightarrow> q \<in> P \<Longrightarrow> disjnt p q \<Longrightarrow> disjnt (f ` p) (f ` q)" for p q
     using f[THEN inj_onD] P[THEN partition_onD1] by (auto simp: disjnt_def)