1.1 --- a/src/HOL/Auth/Message.ML	Mon Dec 16 10:40:14 1996 +0100
     1.2 +++ b/src/HOL/Auth/Message.ML	Mon Dec 16 10:41:26 1996 +0100
     1.3 @@ -803,10 +803,19 @@
     1.4  						 impOfSubs analz_subset_parts]) 2 1))
     1.5         ]) i);
     1.6  
     1.7 -(*Useful in many uniqueness proofs*)
     1.8 +(** Useful in many uniqueness proofs **)
     1.9  fun ex_strip_tac i = REPEAT (swap_res_tac [exI, conjI] i) THEN 
    1.10                       assume_tac (i+1);
    1.11  
    1.12 +(*Apply the EX-ALL quantifification to prove uniqueness theorems in 
    1.13 +  their standard form*)
    1.14 +fun prove_unique_tac lemma = 
    1.15 +  EVERY' [dtac lemma,
    1.16 +	  REPEAT o (mp_tac ORELSE' eresolve_tac [asm_rl,exE]),
    1.17 +	  (*Duplicate the assumption*)
    1.18 +	  forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl,
    1.19 +	  fast_tac (!claset addSDs [spec])];
    1.20 +
    1.21  
    1.22  (*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*)
    1.23  goal Set.thy "A Un (B Un A) = B Un A";