src/HOL/Auth/NS_Public_Bad.thy
changeset 2549 0c723635b9e6
parent 2516 4d68fbe6378b
child 3465 e85c24717cad
--- 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*)