src/HOL/Auth/NS_Public.thy

--- a/src/HOL/Auth/NS_Public.thy	Sat Apr 26 12:38:17 2003 +0200
+++ b/src/HOL/Auth/NS_Public.thy	Sat Apr 26 12:38:42 2003 +0200
@@ -50,7 +50,8 @@
 apply (intro exI bexI)
 apply (rule_tac [2] ns_public.Nil [THEN ns_public.NS1, THEN ns_public.NS2, 
                                    THEN ns_public.NS3])
-by possibility
+apply possibility
+done
 
 
 (**** Inductive proofs about ns_public ****)