src/HOL/Auth/NS_Public_Bad.thy

--- a/src/HOL/Auth/NS_Public_Bad.thy	Wed Mar 28 13:40:06 2001 +0200
+++ b/src/HOL/Auth/NS_Public_Bad.thy	Thu Mar 29 10:44:37 2001 +0200
@@ -43,8 +43,6 @@
            Says B' A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs3\<rbrakk>
           \<Longrightarrow> Says A B (Crypt (pubK B) (Nonce NB)) # evs3 \<in> ns_public"
 
-  (*No Oops message.  Should there be one?*)
-
 declare knows_Spy_partsEs [elim]
 declare analz_subset_parts [THEN subsetD, dest]
 declare Fake_parts_insert [THEN subsetD, dest]