src/HOL/Auth/NS_Public.thy

--- a/src/HOL/Auth/NS_Public.thy	Thu Jan 23 18:10:29 1997 +0100
+++ b/src/HOL/Auth/NS_Public.thy	Thu Jan 23 18:13:07 1997 +0100
@@ -9,8 +9,9 @@
 
 NS_Public = Public + 
 
-consts  lost    :: agent set        (*No need for it to be a variable*)
+consts  lost       :: agent set        (*No need for it to be a variable*)
 	ns_public  :: event list set
+
 inductive ns_public
   intrs 
          (*Initial trace is empty*)