src/HOL/Auth/Shared.ML

 
 Goal "A <= - (range shrK) ==> shrK x ~: A";
 by (Blast_tac 1);
 qed "subset_Compl_range";
 
-Goal "insert (Key K) H = Key `` {K} Un H";
+Goal "insert (Key K) H = Key ` {K} Un H";
 by (Blast_tac 1);
 qed "insert_Key_singleton";
 
-Goal "insert (Key K) (Key``KK Un C) = Key `` (insert K KK) Un C";
+Goal "insert (Key K) (Key`KK Un C) = Key ` (insert K KK) Un C";
 by (Blast_tac 1);
 qed "insert_Key_image";
 
 (*Reverse the normal simplification of "image" to build up (not break down)
   the set of keys.  Use analz_insert_eq with (Un_upper2 RS analz_mono) to

 			 insert_Key_singleton, subset_Compl_range,
 			 Key_not_used, insert_Key_image, Un_assoc RS sym]
 			@disj_comms;
 
 (*Lemma for the trivial direction of the if-and-only-if*)
-Goal "(Key K : analz (Key``nE Un H)) --> (K : nE | Key K : analz H)  ==> \
-\        (Key K : analz (Key``nE Un H)) = (K : nE | Key K : analz H)";
+Goal "(Key K : analz (Key`nE Un H)) --> (K : nE | Key K : analz H)  ==> \
+\        (Key K : analz (Key`nE Un H)) = (K : nE | Key K : analz H)";
 by (blast_tac (claset() addIs [impOfSubs analz_mono]) 1);
 qed "analz_image_freshK_lemma";