doc-src/TutorialI/Protocol/Message.thy
changeset 30607 c3d1590debd8
parent 30548 2eef5e71edd6
child 32149 ef59550a55d3
     1.1 --- a/doc-src/TutorialI/Protocol/Message.thy	Fri Mar 20 11:26:59 2009 +0100
     1.2 +++ b/doc-src/TutorialI/Protocol/Message.thy	Fri Mar 20 15:24:18 2009 +0100
     1.3 @@ -1,5 +1,4 @@
     1.4  (*  Title:      HOL/Auth/Message
     1.5 -    ID:         $Id$
     1.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7      Copyright   1996  University of Cambridge
     1.8  
     1.9 @@ -830,9 +829,9 @@
    1.10  (*Prove base case (subgoal i) and simplify others.  A typical base case
    1.11    concerns  Crypt K X \<notin> Key`shrK`bad  and cannot be proved by rewriting
    1.12    alone.*)
    1.13 -fun prove_simple_subgoals_tac i = 
    1.14 -    force_tac (claset(), simpset() addsimps [@{thm image_eq_UN}]) i THEN
    1.15 -    ALLGOALS Asm_simp_tac
    1.16 +fun prove_simple_subgoals_tac (cs, ss) i = 
    1.17 +    force_tac (cs, ss addsimps [@{thm image_eq_UN}]) i THEN
    1.18 +    ALLGOALS (asm_simp_tac ss)
    1.19  
    1.20  (*Analysis of Fake cases.  Also works for messages that forward unknown parts,
    1.21    but this application is no longer necessary if analz_insert_eq is used.
    1.22 @@ -857,8 +856,7 @@
    1.23  		  (cs addIs [analz_insertI,
    1.24  				   impOfSubs analz_subset_parts]) 4 1))
    1.25  
    1.26 -(*The explicit claset and simpset arguments help it work with Isar*)
    1.27 -fun gen_spy_analz_tac (cs,ss) i =
    1.28 +fun spy_analz_tac (cs,ss) i =
    1.29    DETERM
    1.30     (SELECT_GOAL
    1.31       (EVERY 
    1.32 @@ -870,8 +868,6 @@
    1.33         simp_tac ss 1,
    1.34         REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])),
    1.35         DEPTH_SOLVE (atomic_spy_analz_tac (cs,ss) 1)]) i)
    1.36 -
    1.37 -fun spy_analz_tac i = gen_spy_analz_tac (claset(), simpset()) i
    1.38  *}
    1.39  
    1.40  text{*By default only @{text o_apply} is built-in.  But in the presence of
    1.41 @@ -919,7 +915,7 @@
    1.42  lemmas Fake_parts_sing_imp_Un = Fake_parts_sing [THEN [2] rev_subsetD]
    1.43  
    1.44  method_setup spy_analz = {*
    1.45 -    Scan.succeed (SIMPLE_METHOD' o gen_spy_analz_tac o local_clasimpset_of) *}
    1.46 +    Scan.succeed (SIMPLE_METHOD' o spy_analz_tac o local_clasimpset_of) *}
    1.47      "for proving the Fake case when analz is involved"
    1.48  
    1.49  method_setup atomic_spy_analz = {*