--- a/doc-src/TutorialI/Protocol/Message.thy Thu Jul 23 18:44:08 2009 +0200
+++ b/doc-src/TutorialI/Protocol/Message.thy Thu Jul 23 18:44:09 2009 +0200
@@ -915,15 +915,15 @@
lemmas Fake_parts_sing_imp_Un = Fake_parts_sing [THEN [2] rev_subsetD]
method_setup spy_analz = {*
- Scan.succeed (SIMPLE_METHOD' o spy_analz_tac o local_clasimpset_of) *}
+ Scan.succeed (SIMPLE_METHOD' o spy_analz_tac o clasimpset_of) *}
"for proving the Fake case when analz is involved"
method_setup atomic_spy_analz = {*
- Scan.succeed (SIMPLE_METHOD' o atomic_spy_analz_tac o local_clasimpset_of) *}
+ Scan.succeed (SIMPLE_METHOD' o atomic_spy_analz_tac o clasimpset_of) *}
"for debugging spy_analz"
method_setup Fake_insert_simp = {*
- Scan.succeed (SIMPLE_METHOD' o Fake_insert_simp_tac o local_simpset_of) *}
+ Scan.succeed (SIMPLE_METHOD' o Fake_insert_simp_tac o simpset_of) *}
"for debugging spy_analz"