Moved ex_strip_tac to the common part
authorpaulson
Thu Oct 24 10:31:17 1996 +0200 (1996-10-24)
changeset 2122cb302f6c9c06
parent 2121 7e118eb32bdc
child 2123 959f791b6f0f
Moved ex_strip_tac to the common part
src/HOL/Auth/NS_Shared.ML
     1.1 --- a/src/HOL/Auth/NS_Shared.ML	Thu Oct 24 10:30:43 1996 +0200
     1.2 +++ b/src/HOL/Auth/NS_Shared.ML	Thu Oct 24 10:31:17 1996 +0200
     1.3 @@ -387,8 +387,6 @@
     1.4  (** The session key K uniquely identifies the message, if encrypted
     1.5      with a secure key **)
     1.6  
     1.7 -fun ex_strip_tac i = REPEAT (ares_tac [exI, conjI] i) THEN assume_tac (i+1);
     1.8 -
     1.9  goal thy 
    1.10   "!!evs. evs : ns_shared lost ==>                                            \
    1.11  \      EX A' NA' B' X'. ALL A NA B X.                                        \