Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Cosmetic improvements
authorpaulson
Thu, 23 Jan 1997 18:13:07 +0100
changeset 2549 0c723635b9e6
parent 2548 b5d19d99a58d
child 2550 8d8344bcf98a
Cosmetic improvements
src/HOL/Auth/NS_Public.thy file | annotate | diff | comparison | revisions
src/HOL/Auth/NS_Public_Bad.thy file | annotate | diff | comparison | revisions 
--- 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*)
--- 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*)
isabelle