src/HOL/Metis_Examples/Message.thy

 text\<open>Added to simplify arguments to parts, analz and synth.
   NOTE: the UN versions are no longer used!\<close>
 
 
 text\<open>This allows \<open>blast\<close> to simplify occurrences of
-  @{term "parts(G\<union>H)"} in the assumption.\<close>
+  \<^term>\<open>parts(G\<union>H)\<close> in the assumption.\<close>
 lemmas in_parts_UnE = parts_Un [THEN equalityD1, THEN subsetD, THEN UnE]
 declare in_parts_UnE [elim!]
 
 lemma parts_insert_subset: "insert X (parts H) \<subseteq> parts(insert X H)"
 by (blast intro: parts_mono [THEN [2] rev_subsetD])

                insert (Crypt K X) (analz (insert X H))"
 by (intro equalityI lemma1 lemma2)
 
 text\<open>Case analysis: either the message is secure, or it is not! Effective,
 but can cause subgoals to blow up! Use with \<open>if_split\<close>; apparently
-\<open>split_tac\<close> does not cope with patterns such as @{term"analz (insert
-(Crypt K X) H)"}\<close>
+\<open>split_tac\<close> does not cope with patterns such as \<^term>\<open>analz (insert
+(Crypt K X) H)\<close>\<close>
 lemma analz_Crypt_if [simp]:
      "analz (insert (Crypt K X) H) =
           (if (Key (invKey K) \<in> analz H)
            then insert (Crypt K X) (analz (insert X H))
            else insert (Crypt K X) (analz H))"

 text\<open>Monotonicity\<close>
 lemma synth_mono: "G\<subseteq>H ==> synth(G) \<subseteq> synth(H)"
   by (auto, erule synth.induct, auto)
 
 text\<open>NO \<open>Agent_synth\<close>, as any Agent name can be synthesized.
-  The same holds for @{term Number}\<close>
+  The same holds for \<^term>\<open>Number\<close>\<close>
 inductive_cases Nonce_synth [elim!]: "Nonce n \<in> synth H"
 inductive_cases Key_synth   [elim!]: "Key K \<in> synth H"
 inductive_cases Hash_synth  [elim!]: "Hash X \<in> synth H"
 inductive_cases MPair_synth [elim!]: "\<lbrace>X,Y\<rbrace> \<in> synth H"
 inductive_cases Crypt_synth [elim!]: "Crypt K X \<in> synth H"