diff -r e44d86131648 -r 0c18df79b1c8 src/ZF/UNITY/SubstAx.thy
--- a/src/ZF/UNITY/SubstAx.thy	Tue Sep 27 16:51:35 2022 +0100
+++ b/src/ZF/UNITY/SubstAx.thy	Tue Sep 27 17:03:23 2022 +0100
@@ -153,14 +153,14 @@
 done
 
 (** Distributive laws **)
-lemma LeadsTo_Un_distrib: "(F \<in> (A \<union> B) \<longmapsto>w C)  \<longleftrightarrow> (F \<in> A \<longmapsto>w C & F \<in> B \<longmapsto>w C)"
+lemma LeadsTo_Un_distrib: "(F \<in> (A \<union> B) \<longmapsto>w C)  \<longleftrightarrow> (F \<in> A \<longmapsto>w C \<and> F \<in> B \<longmapsto>w C)"
 by (blast intro: LeadsTo_Un LeadsTo_weaken_L)
 
-lemma LeadsTo_UN_distrib: "(F \<in> (\<Union>i \<in> I. A(i)) \<longmapsto>w B) \<longleftrightarrow>  (\<forall>i \<in> I. F \<in> A(i) \<longmapsto>w B) & F \<in> program"
+lemma LeadsTo_UN_distrib: "(F \<in> (\<Union>i \<in> I. A(i)) \<longmapsto>w B) \<longleftrightarrow>  (\<forall>i \<in> I. F \<in> A(i) \<longmapsto>w B) \<and> F \<in> program"
 by (blast dest: LeadsTo_type [THEN subsetD]
              intro: LeadsTo_UN LeadsTo_weaken_L)
 
-lemma LeadsTo_Union_distrib: "(F \<in> \<Union>(S) \<longmapsto>w B)  \<longleftrightarrow>  (\<forall>A \<in> S. F \<in> A \<longmapsto>w B) & F \<in> program"
+lemma LeadsTo_Union_distrib: "(F \<in> \<Union>(S) \<longmapsto>w B)  \<longleftrightarrow>  (\<forall>A \<in> S. F \<in> A \<longmapsto>w B) \<and> F \<in> program"
 by (blast dest: LeadsTo_type [THEN subsetD]
              intro: LeadsTo_Union LeadsTo_weaken_L)
 
@@ -353,7 +353,7 @@
                 ORELSE   (*subgoal may involve LeadsTo, leadsTo or ensures*)
                 REPEAT (ares_tac ctxt [@{thm LeadsTo_Basis}, @{thm leadsTo_Basis},
                                   @{thm EnsuresI}, @{thm ensuresI}] 1),
-            (*now there are two subgoals: co & transient*)
+            (*now there are two subgoals: co \<and> transient*)
             simp_tac (ctxt addsimps (Named_Theorems.get ctxt \<^named_theorems>\<open>program\<close>)) 2,
             Rule_Insts.res_inst_tac ctxt
               [((("act", 0), Position.none), sact)] [] @{thm transientI} 2,