diff -r 4939494ed791 -r ce654b0e6d69 src/HOL/SET_Protocol/Merchant_Registration.thy
--- a/src/HOL/SET_Protocol/Merchant_Registration.thy	Tue Feb 13 14:24:50 2018 +0100
+++ b/src/HOL/SET_Protocol/Merchant_Registration.thy	Thu Feb 15 12:11:00 2018 +0100
@@ -182,14 +182,14 @@
      "[| Gets A \<lbrace> X, cert (CA i) EKi onlyEnc (priSK RCA),
                       cert (CA i) SKi onlySig (priSK RCA)\<rbrace> \<in> set evs;
          evs \<in> set_mr |]
-      ==> EKi = pubEK (CA i) & SKi = pubSK (CA i)"
+      ==> EKi = pubEK (CA i) \<and> SKi = pubSK (CA i)"
 by (blast dest: certificate_valid_pubEK certificate_valid_pubSK)
 
 
 text\<open>Nobody can have used non-existent keys!\<close>
 lemma new_keys_not_used [rule_format,simp]:
      "evs \<in> set_mr
-      ==> Key K \<notin> used evs --> K \<in> symKeys -->
+      ==> Key K \<notin> used evs \<longrightarrow> K \<in> symKeys \<longrightarrow>
           K \<notin> keysFor (parts (knows Spy evs))"
 apply (erule set_mr.induct, simp_all)
 apply (force dest!: usedI keysFor_parts_insert)  \<comment> \<open>Fake\<close>
@@ -203,13 +203,13 @@
 
 lemma gen_new_keys_not_used [rule_format]:
      "evs \<in> set_mr
-      ==> Key K \<notin> used evs --> K \<in> symKeys -->
-          K \<notin> keysFor (parts (Key`KK Un knows Spy evs))"
+      ==> Key K \<notin> used evs \<longrightarrow> K \<in> symKeys \<longrightarrow>
+          K \<notin> keysFor (parts (Key`KK \<union> knows Spy evs))"
 by auto
 
 lemma gen_new_keys_not_analzd:
      "[|Key K \<notin> used evs; K \<in> symKeys; evs \<in> set_mr |]
-      ==> K \<notin> keysFor (analz (Key`KK Un knows Spy evs))"
+      ==> K \<notin> keysFor (analz (Key`KK \<union> knows Spy evs))"
 by (blast intro: keysFor_mono [THEN [2] rev_subsetD]
           dest: gen_new_keys_not_used)
 
@@ -236,14 +236,14 @@
 for other keys aren't needed.\<close>
 
 lemma parts_image_priEK:
-     "[|Key (priEK (CA i)) \<in> parts (Key`KK Un (knows Spy evs));
+     "[|Key (priEK (CA i)) \<in> parts (Key`KK \<union> (knows Spy evs));
         evs \<in> set_mr|] ==> priEK (CA i) \<in> KK | CA i \<in> bad"
 by auto
 
 text\<open>trivial proof because (priEK (CA i)) never appears even in (parts evs)\<close>
 lemma analz_image_priEK:
      "evs \<in> set_mr ==>
-          (Key (priEK (CA i)) \<in> analz (Key`KK Un (knows Spy evs))) =
+          (Key (priEK (CA i)) \<in> analz (Key`KK \<union> (knows Spy evs))) =
           (priEK (CA i) \<in> KK | CA i \<in> bad)"
 by (blast dest!: parts_image_priEK intro: analz_mono [THEN [2] rev_subsetD])
 
@@ -266,22 +266,22 @@
                  Y\<rbrace> \<in> set evs;
         evs \<in> set_mr|]
   ==> (Key merSK \<in> analz (knows Spy evs) | merSK \<notin> range(\<lambda>C. priEK C))
-   &  (Key merEK \<in> analz (knows Spy evs) | merEK \<notin> range(\<lambda>C. priEK C))"
+   \<and>  (Key merEK \<in> analz (knows Spy evs) | merEK \<notin> range(\<lambda>C. priEK C))"
 apply (unfold sign_def)
 apply (blast dest: merK_neq_priEK)
 done
 
 
 lemma Key_analz_image_Key_lemma:
-     "P --> (Key K \<in> analz (Key`KK Un H)) --> (K\<in>KK | Key K \<in> analz H)
+     "P \<longrightarrow> (Key K \<in> analz (Key`KK \<union> H)) \<longrightarrow> (K\<in>KK | Key K \<in> analz H)
       ==>
-      P --> (Key K \<in> analz (Key`KK Un H)) = (K\<in>KK | Key K \<in> analz H)"
+      P \<longrightarrow> (Key K \<in> analz (Key`KK \<union> H)) = (K\<in>KK | Key K \<in> analz H)"
 by (blast intro: analz_mono [THEN [2] rev_subsetD])
 
 lemma symKey_compromise:
      "evs \<in> set_mr ==>
-      (\<forall>SK KK. SK \<in> symKeys \<longrightarrow> (\<forall>K \<in> KK. K \<notin> range(\<lambda>C. priEK C)) -->
-               (Key SK \<in> analz (Key`KK Un (knows Spy evs))) =
+      (\<forall>SK KK. SK \<in> symKeys \<longrightarrow> (\<forall>K \<in> KK. K \<notin> range(\<lambda>C. priEK C)) \<longrightarrow>
+               (Key SK \<in> analz (Key`KK \<union> (knows Spy evs))) =
                (SK \<in> KK | Key SK \<in> analz (knows Spy evs)))"
 apply (erule set_mr.induct)
 apply (safe del: impI intro!: Key_analz_image_Key_lemma [THEN impI])
@@ -299,9 +299,9 @@
 
 lemma symKey_secrecy [rule_format]:
      "[|CA i \<notin> bad; K \<in> symKeys;  evs \<in> set_mr|]
-      ==> \<forall>X m. Says (Merchant m) (CA i) X \<in> set evs -->
-                Key K \<in> parts{X} -->
-                Merchant m \<notin> bad -->
+      ==> \<forall>X m. Says (Merchant m) (CA i) X \<in> set evs \<longrightarrow>
+                Key K \<in> parts{X} \<longrightarrow>
+                Merchant m \<notin> bad \<longrightarrow>
                 Key K \<notin> analz (knows Spy evs)"
 apply (erule set_mr.induct)
 apply (drule_tac [7] msg4_priEK_disj)
@@ -326,7 +326,7 @@
                     cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)\<rbrace> \<in> set evs;
     evs \<in> set_mr |]
   ==> Notes (CA i) (Key merSK) \<in> set evs
-   &  Notes (CA i) (Key merEK) \<in> set evs"
+   \<and>  Notes (CA i) (Key merEK) \<in> set evs"
 apply (erule rev_mp)
 apply (erule set_mr.induct)
 apply (simp_all (no_asm_simp))
@@ -343,7 +343,7 @@
                     cert  M'      merSK    onlySig (priSK (CA i)),
                     cert  M'      merEK'    onlyEnc (priSK (CA i)),
                     cert (CA i) (pubSK(CA i)) onlySig (priSK RCA)\<rbrace> \<in> set evs;
-    evs \<in> set_mr |] ==> M=M' & NM2=NM2' & merEK=merEK'"
+    evs \<in> set_mr |] ==> M=M' \<and> NM2=NM2' \<and> merEK=merEK'"
 apply (erule rev_mp)
 apply (erule rev_mp)
 apply (erule set_mr.induct)
@@ -363,7 +363,7 @@
                      cert  M'      merEK    onlyEnc (priSK (CA i)),
                      cert (CA i) (pubSK(CA i)) onlySig (priSK RCA)\<rbrace> \<in> set evs;
     evs \<in> set_mr |] 
-  ==> M=M' & NM2=NM2' & merSK=merSK'"
+  ==> M=M' \<and> NM2=NM2' \<and> merSK=merSK'"
 apply (erule rev_mp)
 apply (erule rev_mp)
 apply (erule set_mr.induct)