--- a/doc-src/TutorialI/Protocol/Message.thy Fri Mar 20 11:26:59 2009 +0100
+++ b/doc-src/TutorialI/Protocol/Message.thy Fri Mar 20 15:24:18 2009 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/Auth/Message
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1996 University of Cambridge
@@ -830,9 +829,9 @@
(*Prove base case (subgoal i) and simplify others. A typical base case
concerns Crypt K X \<notin> Key`shrK`bad and cannot be proved by rewriting
alone.*)
-fun prove_simple_subgoals_tac i =
- force_tac (claset(), simpset() addsimps [@{thm image_eq_UN}]) i THEN
- ALLGOALS Asm_simp_tac
+fun prove_simple_subgoals_tac (cs, ss) i =
+ force_tac (cs, ss addsimps [@{thm image_eq_UN}]) i THEN
+ ALLGOALS (asm_simp_tac ss)
(*Analysis of Fake cases. Also works for messages that forward unknown parts,
but this application is no longer necessary if analz_insert_eq is used.
@@ -857,8 +856,7 @@
(cs addIs [analz_insertI,
impOfSubs analz_subset_parts]) 4 1))
-(*The explicit claset and simpset arguments help it work with Isar*)
-fun gen_spy_analz_tac (cs,ss) i =
+fun spy_analz_tac (cs,ss) i =
DETERM
(SELECT_GOAL
(EVERY
@@ -870,8 +868,6 @@
simp_tac ss 1,
REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])),
DEPTH_SOLVE (atomic_spy_analz_tac (cs,ss) 1)]) i)
-
-fun spy_analz_tac i = gen_spy_analz_tac (claset(), simpset()) i
*}
text{*By default only @{text o_apply} is built-in. But in the presence of
@@ -919,7 +915,7 @@
lemmas Fake_parts_sing_imp_Un = Fake_parts_sing [THEN [2] rev_subsetD]
method_setup spy_analz = {*
- Scan.succeed (SIMPLE_METHOD' o gen_spy_analz_tac o local_clasimpset_of) *}
+ Scan.succeed (SIMPLE_METHOD' o spy_analz_tac o local_clasimpset_of) *}
"for proving the Fake case when analz is involved"
method_setup atomic_spy_analz = {*