# HG changeset patch
# User paulson
# Date 847358157 -3600
# Node ID 63dfe7f19cadd1b36e4ddd832195c47f36dc4592
# Parent  c87368fc736bf00e2446fe45b5a0a7ffa7b1e875
Deleted bogus comment

diff -r c87368fc736b -r 63dfe7f19cad src/HOL/Auth/NS_Shared.ML
--- a/src/HOL/Auth/NS_Shared.ML	Thu Nov 07 10:11:06 1996 +0100
+++ b/src/HOL/Auth/NS_Shared.ML	Thu Nov 07 10:15:57 1996 +0100
@@ -288,7 +288,6 @@
      (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]
                          @ pushes)
                setloop split_tac [expand_if])));
-(** LEVEL 6 **)
 (*NS3, Fake*) 
 by (EVERY (map spy_analz_tac [5,2]));
 by (REPEAT (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1));