doc-src/TutorialI/Protocol/Message_lemmas.ML

 (*In any message, there is an upper bound N on its greatest nonce.*)
 Goal "\\<exists>N. \\<forall>n. N\\<le>n --> Nonce n \\<notin> parts {msg}";
 by (induct_tac "msg" 1);
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [exI, parts_insert2])));
 (*MPair case: blast_tac works out the necessary sum itself!*)
-by (blast_tac (claset() addSEs [add_leE]) 2);
+by (blast_tac (claset() addSEs [@{thm add_leE}]) 2);
 (*Nonce case*)
 by (res_inst_tac [("x","N + Suc nat")] exI 1);
-by (auto_tac (claset() addSEs [add_leE], simpset()));
+by (auto_tac (claset() addSEs [@{thm add_leE}], simpset()));
 qed "msg_Nonce_supply";
 
 
 (**** Inductive relation "analz" ****)