src/HOL/Auth/Message.thy
changeset 30607 c3d1590debd8
parent 30549 d2d7874648bd
child 32117 0762b9ad83df
     1.1 --- a/src/HOL/Auth/Message.thy	Fri Mar 20 11:26:59 2009 +0100
     1.2 +++ b/src/HOL/Auth/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 @@ -848,9 +847,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 @@ -875,8 +874,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 @@ -888,8 +886,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  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 Message.gen_spy_analz_tac o local_clasimpset_of) *}
    1.46 +    Scan.succeed (SIMPLE_METHOD' o Message.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 = {*