src/HOL/SET-Protocol/MessageSET.thy
changeset 30607 c3d1590debd8
parent 30549 d2d7874648bd
child 32117 0762b9ad83df
     1.1 --- a/src/HOL/SET-Protocol/MessageSET.thy	Fri Mar 20 11:26:59 2009 +0100
     1.2 +++ b/src/HOL/SET-Protocol/MessageSET.thy	Fri Mar 20 15:24:18 2009 +0100
     1.3 @@ -1,5 +1,4 @@
     1.4  (*  Title:      HOL/Auth/SET/MessageSET
     1.5 -    ID:         $Id$
     1.6      Authors:     Giampaolo Bella, Fabio Massacci, Lawrence C Paulson
     1.7  *)
     1.8  
     1.9 @@ -846,9 +845,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 -    CLASIMPSET' (fn (cs, ss) => force_tac (cs, ss addsimps [@{thm image_eq_UN}])) i THEN
    1.15 -    ALLGOALS (SIMPSET' 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 @@ -873,8 +872,7 @@
    1.23  		  (cs addIs [@{thm analz_insertI},
    1.24  				   impOfSubs @{thm 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 @@ -887,8 +885,6 @@
    1.33         REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])),
    1.34         DEPTH_SOLVE (atomic_spy_analz_tac (cs,ss) 1)]) i)
    1.35  
    1.36 -val spy_analz_tac = CLASIMPSET' gen_spy_analz_tac;
    1.37 -
    1.38  end
    1.39  *}
    1.40  (*>*)
    1.41 @@ -941,7 +937,7 @@
    1.42  
    1.43  method_setup spy_analz = {*
    1.44      Scan.succeed (fn ctxt =>
    1.45 -        SIMPLE_METHOD' (MessageSET.gen_spy_analz_tac (local_clasimpset_of ctxt))) *}
    1.46 +        SIMPLE_METHOD' (MessageSET.spy_analz_tac (local_clasimpset_of ctxt))) *}
    1.47      "for proving the Fake case when analz is involved"
    1.48  
    1.49  method_setup atomic_spy_analz = {*