# HG changeset patch
# User haftmann
# Date 1185002056 -7200
# Node ID 4127c1d910f15ce83e362d9e2944797c99bdec35
# Parent  9a75e9772761d83d355144fff1607028770d36e5
dropped Nat legacy bindings

diff -r 9a75e9772761 -r 4127c1d910f1 doc-src/TutorialI/Protocol/Event_lemmas.ML
--- 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*)
diff -r 9a75e9772761 -r 4127c1d910f1 doc-src/TutorialI/Protocol/Message_lemmas.ML
--- 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";
 
 
diff -r 9a75e9772761 -r 4127c1d910f1 doc-src/TutorialI/Protocol/Public_lemmas.ML
--- 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";