# HG changeset patch
# User paulson
# Date 854039587 -3600
# Node ID 0c723635b9e6534dea6ae057ad8535b912299aaf
# Parent  b5d19d99a58dadb15a39cc309d60bc0618f9e319
Cosmetic improvements

diff -r b5d19d99a58d -r 0c723635b9e6 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*)
diff -r b5d19d99a58d -r 0c723635b9e6 src/HOL/Auth/NS_Public_Bad.thy
--- a/src/HOL/Auth/NS_Public_Bad.thy	Thu Jan 23 18:10:29 1997 +0100
+++ b/src/HOL/Auth/NS_Public_Bad.thy	Thu Jan 23 18:13:07 1997 +0100
@@ -13,8 +13,9 @@
 
 NS_Public_Bad = 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*)