--- a/doc-src/TutorialI/Protocol/Event_lemmas.ML Fri Jul 20 19:54:03 2007 +0200
+++ b/doc-src/TutorialI/Protocol/Event_lemmas.ML Sat Jul 21 09:14:16 2007 +0200
@@ -223,7 +223,7 @@
parts_trans,
Says_imp_knows_Spy RS analz.Inj,
impOfSubs analz_mono, analz_cut]
- addIs [less_SucI]) i;
+ addIs [@{thm less_SucI}]) i;
(*Compatibility for the old "spies" function*)
--- a/doc-src/TutorialI/Protocol/Message_lemmas.ML Fri Jul 20 19:54:03 2007 +0200
+++ b/doc-src/TutorialI/Protocol/Message_lemmas.ML Sat Jul 21 09:14:16 2007 +0200
@@ -330,10 +330,10 @@
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";
--- a/doc-src/TutorialI/Protocol/Public_lemmas.ML Fri Jul 20 19:54:03 2007 +0200
+++ b/doc-src/TutorialI/Protocol/Public_lemmas.ML Sat Jul 21 09:14:16 2007 +0200
@@ -125,7 +125,7 @@
addsplits [expand_event_case])));
by Safe_tac;
by (ALLGOALS (rtac (msg_Nonce_supply RS exE)));
-by (ALLGOALS (blast_tac (claset() addSEs [add_leE])));
+by (ALLGOALS (blast_tac (claset() addSEs [@{thm add_leE}])));
val lemma = result();
Goal "EX N. Nonce N ~: used evs";