--- a/src/ZF/UNITY/Monotonicity.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/ZF/UNITY/Monotonicity.thy Wed Jan 10 15:25:09 2018 +0100
@@ -102,7 +102,7 @@
(** Monotonicity of \<union> **)
lemma mono_Un [iff]:
- "mono2(Pow(A), SetLe(A), Pow(A), SetLe(A), Pow(A), SetLe(A), op Un)"
+ "mono2(Pow(A), SetLe(A), Pow(A), SetLe(A), Pow(A), SetLe(A), (Un))"
by (unfold mono2_def SetLe_def, auto)
(* Monotonicity of multiset union *)
@@ -117,4 +117,4 @@
lemma mono_succ [iff]: "mono1(nat, Le, nat, Le, succ)"
by (unfold mono1_def Le_def, auto)
-end
\ No newline at end of file
+end