1.1 --- a/doc-src/TutorialI/Protocol/Event_lemmas.ML	Fri Jul 20 19:54:03 2007 +0200
     1.2 +++ b/doc-src/TutorialI/Protocol/Event_lemmas.ML	Sat Jul 21 09:14:16 2007 +0200
     1.3 @@ -223,7 +223,7 @@
     1.4  			       parts_trans,
     1.5                                 Says_imp_knows_Spy RS analz.Inj,
     1.6                                 impOfSubs analz_mono, analz_cut] 
     1.7 -                        addIs [less_SucI]) i;
     1.8 +                        addIs [@{thm less_SucI}]) i;
     1.9  
    1.10  
    1.11  (*Compatibility for the old "spies" function*)

     2.1 --- a/doc-src/TutorialI/Protocol/Message_lemmas.ML	Fri Jul 20 19:54:03 2007 +0200
     2.2 +++ b/doc-src/TutorialI/Protocol/Message_lemmas.ML	Sat Jul 21 09:14:16 2007 +0200
     2.3 @@ -330,10 +330,10 @@
     2.4  by (induct_tac "msg" 1);
     2.5  by (ALLGOALS (asm_simp_tac (simpset() addsimps [exI, parts_insert2])));
     2.6  (*MPair case: blast_tac works out the necessary sum itself!*)
     2.7 -by (blast_tac (claset() addSEs [add_leE]) 2);
     2.8 +by (blast_tac (claset() addSEs [@{thm add_leE}]) 2);
     2.9  (*Nonce case*)
    2.10  by (res_inst_tac [("x","N + Suc nat")] exI 1);
    2.11 -by (auto_tac (claset() addSEs [add_leE], simpset()));
    2.12 +by (auto_tac (claset() addSEs [@{thm add_leE}], simpset()));
    2.13  qed "msg_Nonce_supply";
    2.14  
    2.15  

     3.1 --- a/doc-src/TutorialI/Protocol/Public_lemmas.ML	Fri Jul 20 19:54:03 2007 +0200
     3.2 +++ b/doc-src/TutorialI/Protocol/Public_lemmas.ML	Sat Jul 21 09:14:16 2007 +0200
     3.3 @@ -125,7 +125,7 @@
     3.4  			addsplits [expand_event_case])));
     3.5  by Safe_tac;
     3.6  by (ALLGOALS (rtac (msg_Nonce_supply RS exE)));
     3.7 -by (ALLGOALS (blast_tac (claset() addSEs [add_leE])));
     3.8 +by (ALLGOALS (blast_tac (claset() addSEs [@{thm add_leE}])));
     3.9  val lemma = result();
    3.10  
    3.11  Goal "EX N. Nonce N ~: used evs";