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.
updated some headers;
authorwenzelm
Thu, 22 Jul 2010 18:08:39 +0200
changeset 37936 1e4c5015a72e
parent 37935 7551769de556
child 37937 9e482a3e651e
child 37945 32f9b7a70fc0
updated some headers;
src/HOL/Auth/CertifiedEmail.thy file | annotate | diff | comparison | revisions
src/HOL/Auth/Event.thy file | annotate | diff | comparison | revisions
src/HOL/Auth/KerberosIV.thy file | annotate | diff | comparison | revisions
src/HOL/Auth/KerberosIV_Gets.thy file | annotate | diff | comparison | revisions
src/HOL/Auth/KerberosV.thy file | annotate | diff | comparison | revisions
src/HOL/Auth/Kerberos_BAN.thy file | annotate | diff | comparison | revisions
src/HOL/Auth/Kerberos_BAN_Gets.thy file | annotate | diff | comparison | revisions
src/HOL/Auth/Message.thy file | annotate | diff | comparison | revisions
src/HOL/Auth/NS_Public.thy file | annotate | diff | comparison | revisions
src/HOL/Auth/NS_Public_Bad.thy file | annotate | diff | comparison | revisions
src/HOL/Auth/NS_Shared.thy file | annotate | diff | comparison | revisions
src/HOL/Auth/OtwayRees.thy file | annotate | diff | comparison | revisions
src/HOL/Auth/OtwayReesBella.thy file | annotate | diff | comparison | revisions
src/HOL/Auth/OtwayRees_AN.thy file | annotate | diff | comparison | revisions
src/HOL/Auth/OtwayRees_Bad.thy file | annotate | diff | comparison | revisions
src/HOL/Auth/Public.thy file | annotate | diff | comparison | revisions
src/HOL/Auth/Recur.thy file | annotate | diff | comparison | revisions
src/HOL/Auth/Shared.thy file | annotate | diff | comparison | revisions
src/HOL/Auth/TLS.thy file | annotate | diff | comparison | revisions
src/HOL/Auth/WooLam.thy file | annotate | diff | comparison | revisions
src/HOL/Auth/Yahalom.thy file | annotate | diff | comparison | revisions
src/HOL/Auth/Yahalom2.thy file | annotate | diff | comparison | revisions
src/HOL/Auth/Yahalom_Bad.thy file | annotate | diff | comparison | revisions
src/HOL/Auth/ZhouGollmann.thy file | annotate | diff | comparison | revisions
src/HOL/UNITY/Comp/Alloc.thy file | annotate | diff | comparison | revisions
src/HOL/UNITY/Comp/Handshake.thy file | annotate | diff | comparison | revisions
src/HOL/UNITY/Comp/Priority.thy file | annotate | diff | comparison | revisions
src/HOL/UNITY/Comp/PriorityAux.thy file | annotate | diff | comparison | revisions
src/HOL/UNITY/Comp/Progress.thy file | annotate | diff | comparison | revisions
src/HOL/UNITY/Comp/TimerArray.thy file | annotate | diff | comparison | revisions
src/HOL/UNITY/Detects.thy file | annotate | diff | comparison | revisions
src/HOL/UNITY/FP.thy file | annotate | diff | comparison | revisions
src/HOL/UNITY/Rename.thy file | annotate | diff | comparison | revisions
src/HOL/UNITY/Simple/Channel.thy file | annotate | diff | comparison | revisions
src/HOL/UNITY/Simple/Common.thy file | annotate | diff | comparison | revisions
src/HOL/UNITY/Simple/Deadlock.thy file | annotate | diff | comparison | revisions
src/HOL/UNITY/Simple/Lift.thy file | annotate | diff | comparison | revisions
src/HOL/UNITY/Simple/Mutex.thy file | annotate | diff | comparison | revisions
src/HOL/UNITY/Simple/NSP_Bad.thy file | annotate | diff | comparison | revisions
src/HOL/UNITY/Simple/Network.thy file | annotate | diff | comparison | revisions
src/HOL/UNITY/Simple/Reach.thy file | annotate | diff | comparison | revisions
src/HOL/UNITY/Simple/Reachability.thy file | annotate | diff | comparison | revisions
src/HOL/UNITY/Simple/Token.thy file | annotate | diff | comparison | revisions
src/HOL/UNITY/SubstAx.thy file | annotate | diff | comparison | revisions
src/HOL/UNITY/Transformers.thy file | annotate | diff | comparison | revisions
src/HOL/UNITY/UNITY_tactics.ML file | annotate | diff | comparison | revisions
src/HOL/UNITY/WFair.thy file | annotate | diff | comparison | revisions
src/ZF/UNITY/MultisetSum.thy file | annotate | diff | comparison | revisions
src/ZF/UNITY/State.thy file | annotate | diff | comparison | revisions
src/ZF/UNITY/WFair.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Auth/CertifiedEmail.thy	Thu Jul 22 17:26:31 2010 +0200
+++ b/src/HOL/Auth/CertifiedEmail.thy	Thu Jul 22 18:08:39 2010 +0200
@@ -1,5 +1,4 @@
-(*  Title:      HOL/Auth/CertifiedEmail
-    ID:         $Id$
+(*  Title:      HOL/Auth/CertifiedEmail.thy
     Author:     Giampaolo Bella, Christiano Longo and Lawrence C Paulson
 *)
 
--- a/src/HOL/Auth/Event.thy	Thu Jul 22 17:26:31 2010 +0200
+++ b/src/HOL/Auth/Event.thy	Thu Jul 22 18:08:39 2010 +0200
@@ -1,5 +1,4 @@
-(*  Title:      HOL/Auth/Event
-    ID:         $Id$
+(*  Title:      HOL/Auth/Event.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1996  University of Cambridge
 
--- a/src/HOL/Auth/KerberosIV.thy	Thu Jul 22 17:26:31 2010 +0200
+++ b/src/HOL/Auth/KerberosIV.thy	Thu Jul 22 18:08:39 2010 +0200
@@ -1,5 +1,4 @@
-(*  Title:      HOL/Auth/KerberosIV
-    ID:         $Id$
+(*  Title:      HOL/Auth/KerberosIV.thy
     Author:     Giampaolo Bella, Cambridge University Computer Laboratory
     Copyright   1998  University of Cambridge
 *)
--- a/src/HOL/Auth/KerberosIV_Gets.thy	Thu Jul 22 17:26:31 2010 +0200
+++ b/src/HOL/Auth/KerberosIV_Gets.thy	Thu Jul 22 18:08:39 2010 +0200
@@ -1,5 +1,4 @@
-(*  Title:      HOL/Auth/KerberosIV
-    ID:         $Id$
+(*  Title:      HOL/Auth/KerberosIV_Gets.thy
     Author:     Giampaolo Bella, Cambridge University Computer Laboratory
     Copyright   1998  University of Cambridge
 *)
--- a/src/HOL/Auth/KerberosV.thy	Thu Jul 22 17:26:31 2010 +0200
+++ b/src/HOL/Auth/KerberosV.thy	Thu Jul 22 18:08:39 2010 +0200
@@ -1,4 +1,4 @@
-(*  ID:         $Id$
+(*  Title:      HOL/Auth/KerberosV.thy
     Author:     Giampaolo Bella, Catania University
 *)
 
--- a/src/HOL/Auth/Kerberos_BAN.thy	Thu Jul 22 17:26:31 2010 +0200
+++ b/src/HOL/Auth/Kerberos_BAN.thy	Thu Jul 22 18:08:39 2010 +0200
@@ -1,5 +1,4 @@
-(*  Title:      HOL/Auth/Kerberos_BAN
-    ID:         $Id$
+(*  Title:      HOL/Auth/Kerberos_BAN.thy
     Author:     Giampaolo Bella, Cambridge University Computer Laboratory
     Copyright   1998  University of Cambridge
 *)
--- a/src/HOL/Auth/Kerberos_BAN_Gets.thy	Thu Jul 22 17:26:31 2010 +0200
+++ b/src/HOL/Auth/Kerberos_BAN_Gets.thy	Thu Jul 22 18:08:39 2010 +0200
@@ -1,4 +1,4 @@
-(*  ID:         $Id$
+(*  Title:      HOL/Auth/Kerberos_BAN_Gets.thy
     Author:     Giampaolo Bella, Catania University
 *)
 
--- a/src/HOL/Auth/Message.thy	Thu Jul 22 17:26:31 2010 +0200
+++ b/src/HOL/Auth/Message.thy	Thu Jul 22 18:08:39 2010 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Auth/Message
+(*  Title:      HOL/Auth/Message.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1996  University of Cambridge
 
--- a/src/HOL/Auth/NS_Public.thy	Thu Jul 22 17:26:31 2010 +0200
+++ b/src/HOL/Auth/NS_Public.thy	Thu Jul 22 18:08:39 2010 +0200
@@ -1,5 +1,4 @@
-(*  Title:      HOL/Auth/NS_Public
-    ID:         $Id$
+(*  Title:      HOL/Auth/NS_Public.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1996  University of Cambridge
 
--- a/src/HOL/Auth/NS_Public_Bad.thy	Thu Jul 22 17:26:31 2010 +0200
+++ b/src/HOL/Auth/NS_Public_Bad.thy	Thu Jul 22 18:08:39 2010 +0200
@@ -1,5 +1,4 @@
-(*  Title:      HOL/Auth/NS_Public_Bad
-    ID:         $Id$
+(*  Title:      HOL/Auth/NS_Public_Bad.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1996  University of Cambridge
 
--- a/src/HOL/Auth/NS_Shared.thy	Thu Jul 22 17:26:31 2010 +0200
+++ b/src/HOL/Auth/NS_Shared.thy	Thu Jul 22 18:08:39 2010 +0200
@@ -1,5 +1,4 @@
-(*  Title:      HOL/Auth/NS_Shared
-    ID:         $Id$
+(*  Title:      HOL/Auth/NS_Shared.thy
     Author:     Lawrence C Paulson and Giampaolo Bella 
     Copyright   1996  University of Cambridge
 *)
--- a/src/HOL/Auth/OtwayRees.thy	Thu Jul 22 17:26:31 2010 +0200
+++ b/src/HOL/Auth/OtwayRees.thy	Thu Jul 22 18:08:39 2010 +0200
@@ -1,5 +1,4 @@
-(*  Title:      HOL/Auth/OtwayRees
-    ID:         $Id$
+(*  Title:      HOL/Auth/OtwayRees.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1996  University of Cambridge
 *)
--- a/src/HOL/Auth/OtwayReesBella.thy	Thu Jul 22 17:26:31 2010 +0200
+++ b/src/HOL/Auth/OtwayReesBella.thy	Thu Jul 22 18:08:39 2010 +0200
@@ -1,4 +1,4 @@
-(*  ID:         $Id$
+(*  Title:      HOL/Auth/OtwayReesBella.thy
     Author:     Giampaolo Bella, Catania University
 *)
 
--- a/src/HOL/Auth/OtwayRees_AN.thy	Thu Jul 22 17:26:31 2010 +0200
+++ b/src/HOL/Auth/OtwayRees_AN.thy	Thu Jul 22 18:08:39 2010 +0200
@@ -1,5 +1,4 @@
-(*  Title:      HOL/Auth/OtwayRees
-    ID:         $Id$
+(*  Title:      HOL/Auth/OtwayRees_AN.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1996  University of Cambridge
 *)
--- a/src/HOL/Auth/OtwayRees_Bad.thy	Thu Jul 22 17:26:31 2010 +0200
+++ b/src/HOL/Auth/OtwayRees_Bad.thy	Thu Jul 22 18:08:39 2010 +0200
@@ -1,5 +1,4 @@
-(*  Title:      HOL/Auth/OtwayRees_Bad
-    ID:         $Id$
+(*  Title:      HOL/Auth/OtwayRees_Bad.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1996  University of Cambridge
 *)
--- a/src/HOL/Auth/Public.thy	Thu Jul 22 17:26:31 2010 +0200
+++ b/src/HOL/Auth/Public.thy	Thu Jul 22 18:08:39 2010 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Auth/Public
+(*  Title:      HOL/Auth/Public.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1996  University of Cambridge
 
--- a/src/HOL/Auth/Recur.thy	Thu Jul 22 17:26:31 2010 +0200
+++ b/src/HOL/Auth/Recur.thy	Thu Jul 22 18:08:39 2010 +0200
@@ -1,5 +1,4 @@
-(*  Title:      HOL/Auth/Recur
-    ID:         $Id$
+(*  Title:      HOL/Auth/Recur.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1996  University of Cambridge
 *)
--- a/src/HOL/Auth/Shared.thy	Thu Jul 22 17:26:31 2010 +0200
+++ b/src/HOL/Auth/Shared.thy	Thu Jul 22 18:08:39 2010 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Auth/Shared
+(*  Title:      HOL/Auth/Shared.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1996  University of Cambridge
 
--- a/src/HOL/Auth/TLS.thy	Thu Jul 22 17:26:31 2010 +0200
+++ b/src/HOL/Auth/TLS.thy	Thu Jul 22 18:08:39 2010 +0200
@@ -1,5 +1,4 @@
-(*  Title:      HOL/Auth/TLS
-    ID:         $Id$
+(*  Title:      HOL/Auth/TLS.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1997  University of Cambridge
 
--- a/src/HOL/Auth/WooLam.thy	Thu Jul 22 17:26:31 2010 +0200
+++ b/src/HOL/Auth/WooLam.thy	Thu Jul 22 18:08:39 2010 +0200
@@ -1,5 +1,4 @@
-(*  Title:      HOL/Auth/WooLam
-    ID:         $Id$
+(*  Title:      HOL/Auth/WooLam.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1996  University of Cambridge
 *)
--- a/src/HOL/Auth/Yahalom.thy	Thu Jul 22 17:26:31 2010 +0200
+++ b/src/HOL/Auth/Yahalom.thy	Thu Jul 22 18:08:39 2010 +0200
@@ -1,5 +1,4 @@
-(*  Title:      HOL/Auth/Yahalom
-    ID:         $Id$
+(*  Title:      HOL/Auth/Yahalom.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1996  University of Cambridge
 *)
--- a/src/HOL/Auth/Yahalom2.thy	Thu Jul 22 17:26:31 2010 +0200
+++ b/src/HOL/Auth/Yahalom2.thy	Thu Jul 22 18:08:39 2010 +0200
@@ -1,5 +1,4 @@
-(*  Title:      HOL/Auth/Yahalom2
-    ID:         $Id$
+(*  Title:      HOL/Auth/Yahalom2.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1996  University of Cambridge
 *)
--- a/src/HOL/Auth/Yahalom_Bad.thy	Thu Jul 22 17:26:31 2010 +0200
+++ b/src/HOL/Auth/Yahalom_Bad.thy	Thu Jul 22 18:08:39 2010 +0200
@@ -1,5 +1,4 @@
-(*  Title:      HOL/Auth/Yahalom
-    ID:         $Id$
+(*  Title:      HOL/Auth/Yahalom_Bad.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1996  University of Cambridge
 *)
--- a/src/HOL/Auth/ZhouGollmann.thy	Thu Jul 22 17:26:31 2010 +0200
+++ b/src/HOL/Auth/ZhouGollmann.thy	Thu Jul 22 18:08:39 2010 +0200
@@ -1,5 +1,4 @@
-(*  Title:      HOL/Auth/ZhouGollmann
-    ID:         $Id$
+(*  Title:      HOL/Auth/ZhouGollmann.thy
     Author:     Giampaolo Bella and L C Paulson, Cambridge Univ Computer Lab
     Copyright   2003  University of Cambridge
 
--- a/src/HOL/UNITY/Comp/Alloc.thy	Thu Jul 22 17:26:31 2010 +0200
+++ b/src/HOL/UNITY/Comp/Alloc.thy	Thu Jul 22 18:08:39 2010 +0200
@@ -1,4 +1,4 @@
-(*  ID:         $Id$
+(*  Title:      HOL/UNITY/Comp/Alloc.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1998  University of Cambridge
 
--- a/src/HOL/UNITY/Comp/Handshake.thy	Thu Jul 22 17:26:31 2010 +0200
+++ b/src/HOL/UNITY/Comp/Handshake.thy	Thu Jul 22 18:08:39 2010 +0200
@@ -1,5 +1,4 @@
-(*  Title:      HOL/UNITY/Handshake.thy
-    ID:         $Id$
+(*  Title:      HOL/UNITY/Comp/Handshake.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1998  University of Cambridge
 
--- a/src/HOL/UNITY/Comp/Priority.thy	Thu Jul 22 17:26:31 2010 +0200
+++ b/src/HOL/UNITY/Comp/Priority.thy	Thu Jul 22 18:08:39 2010 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/UNITY/Priority
+(*  Title:      HOL/UNITY/Comp/Priority.thy
     Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
     Copyright   2001  University of Cambridge
 *)
--- a/src/HOL/UNITY/Comp/PriorityAux.thy	Thu Jul 22 17:26:31 2010 +0200
+++ b/src/HOL/UNITY/Comp/PriorityAux.thy	Thu Jul 22 18:08:39 2010 +0200
@@ -1,5 +1,4 @@
-(*  Title:      HOL/UNITY/PriorityAux
-    ID:         $Id$
+(*  Title:      HOL/UNITY/Comp/PriorityAux.thy
     Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
     Copyright   2001  University of Cambridge
 
--- a/src/HOL/UNITY/Comp/Progress.thy	Thu Jul 22 17:26:31 2010 +0200
+++ b/src/HOL/UNITY/Comp/Progress.thy	Thu Jul 22 18:08:39 2010 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/UNITY/Progress
+(*  Title:      HOL/UNITY/Comp/Progress.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   2003  University of Cambridge
 
--- a/src/HOL/UNITY/Comp/TimerArray.thy	Thu Jul 22 17:26:31 2010 +0200
+++ b/src/HOL/UNITY/Comp/TimerArray.thy	Thu Jul 22 18:08:39 2010 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/UNITY/TimerArray.thy
+(*  Title:      HOL/UNITY/Comp/TimerArray.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1998  University of Cambridge
 
--- a/src/HOL/UNITY/Detects.thy	Thu Jul 22 17:26:31 2010 +0200
+++ b/src/HOL/UNITY/Detects.thy	Thu Jul 22 18:08:39 2010 +0200
@@ -1,5 +1,4 @@
-(*  Title:      HOL/UNITY/Detects
-    ID:         $Id$
+(*  Title:      HOL/UNITY/Detects.thy
     Author:     Tanja Vos, Cambridge University Computer Laboratory
     Copyright   2000  University of Cambridge
 
--- a/src/HOL/UNITY/FP.thy	Thu Jul 22 17:26:31 2010 +0200
+++ b/src/HOL/UNITY/FP.thy	Thu Jul 22 18:08:39 2010 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/UNITY/FP
+(*  Title:      HOL/UNITY/FP.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1998  University of Cambridge
 
--- a/src/HOL/UNITY/Rename.thy	Thu Jul 22 17:26:31 2010 +0200
+++ b/src/HOL/UNITY/Rename.thy	Thu Jul 22 18:08:39 2010 +0200
@@ -1,5 +1,4 @@
 (*  Title:      HOL/UNITY/Rename.thy
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   2000  University of Cambridge
 *)
--- a/src/HOL/UNITY/Simple/Channel.thy	Thu Jul 22 17:26:31 2010 +0200
+++ b/src/HOL/UNITY/Simple/Channel.thy	Thu Jul 22 18:08:39 2010 +0200
@@ -1,5 +1,4 @@
-(*  Title:      HOL/UNITY/Channel
-    ID:         $Id$
+(*  Title:      HOL/UNITY/Simple/Channel.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1998  University of Cambridge
 
--- a/src/HOL/UNITY/Simple/Common.thy	Thu Jul 22 17:26:31 2010 +0200
+++ b/src/HOL/UNITY/Simple/Common.thy	Thu Jul 22 18:08:39 2010 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/UNITY/Common
+(*  Title:      HOL/UNITY/Simple/Common.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1998  University of Cambridge
 
--- a/src/HOL/UNITY/Simple/Deadlock.thy	Thu Jul 22 17:26:31 2010 +0200
+++ b/src/HOL/UNITY/Simple/Deadlock.thy	Thu Jul 22 18:08:39 2010 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/UNITY/Deadlock.thy
+(*  Title:      HOL/UNITY/Simple/Deadlock.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1998  University of Cambridge
 
--- a/src/HOL/UNITY/Simple/Lift.thy	Thu Jul 22 17:26:31 2010 +0200
+++ b/src/HOL/UNITY/Simple/Lift.thy	Thu Jul 22 18:08:39 2010 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/UNITY/Lift.thy
+(*  Title:      HOL/UNITY/Simple/Lift.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1998  University of Cambridge
 
--- a/src/HOL/UNITY/Simple/Mutex.thy	Thu Jul 22 17:26:31 2010 +0200
+++ b/src/HOL/UNITY/Simple/Mutex.thy	Thu Jul 22 18:08:39 2010 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/UNITY/Mutex.thy
+(*  Title:      HOL/UNITY/Simple/Mutex.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1998  University of Cambridge
 
--- a/src/HOL/UNITY/Simple/NSP_Bad.thy	Thu Jul 22 17:26:31 2010 +0200
+++ b/src/HOL/UNITY/Simple/NSP_Bad.thy	Thu Jul 22 18:08:39 2010 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Auth/NSP_Bad.thy
+(*  Title:      HOL/UNITY/Simple/NSP_Bad.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1996  University of Cambridge
 
--- a/src/HOL/UNITY/Simple/Network.thy	Thu Jul 22 17:26:31 2010 +0200
+++ b/src/HOL/UNITY/Simple/Network.thy	Thu Jul 22 18:08:39 2010 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/UNITY/Network.thy
+(*  Title:      HOL/UNITY/Simple/Network.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1998  University of Cambridge
 
--- a/src/HOL/UNITY/Simple/Reach.thy	Thu Jul 22 17:26:31 2010 +0200
+++ b/src/HOL/UNITY/Simple/Reach.thy	Thu Jul 22 18:08:39 2010 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/UNITY/Reach.thy
+(*  Title:      HOL/UNITY/Simple/Reach.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1998  University of Cambridge
 
--- a/src/HOL/UNITY/Simple/Reachability.thy	Thu Jul 22 17:26:31 2010 +0200
+++ b/src/HOL/UNITY/Simple/Reachability.thy	Thu Jul 22 18:08:39 2010 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/UNITY/Reachability.thy
+(*  Title:      HOL/UNITY/Simple/Reachability.thy
     Author:     Tanja Vos, Cambridge University Computer Laboratory
     Copyright   2000  University of Cambridge
 
--- a/src/HOL/UNITY/Simple/Token.thy	Thu Jul 22 17:26:31 2010 +0200
+++ b/src/HOL/UNITY/Simple/Token.thy	Thu Jul 22 18:08:39 2010 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/UNITY/Token
+(*  Title:      HOL/UNITY/Simple/Token.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1998  University of Cambridge
 *)
--- a/src/HOL/UNITY/SubstAx.thy	Thu Jul 22 17:26:31 2010 +0200
+++ b/src/HOL/UNITY/SubstAx.thy	Thu Jul 22 18:08:39 2010 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/UNITY/SubstAx
+(*  Title:      HOL/UNITY/SubstAx.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1998  University of Cambridge
 
--- a/src/HOL/UNITY/Transformers.thy	Thu Jul 22 17:26:31 2010 +0200
+++ b/src/HOL/UNITY/Transformers.thy	Thu Jul 22 18:08:39 2010 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/UNITY/Transformers
+(*  Title:      HOL/UNITY/Transformers.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   2003  University of Cambridge
 
--- a/src/HOL/UNITY/UNITY_tactics.ML	Thu Jul 22 17:26:31 2010 +0200
+++ b/src/HOL/UNITY/UNITY_tactics.ML	Thu Jul 22 18:08:39 2010 +0200
@@ -1,5 +1,4 @@
 (*  Title:      HOL/UNITY/UNITY_tactics.ML
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   2003  University of Cambridge
 
--- a/src/HOL/UNITY/WFair.thy	Thu Jul 22 17:26:31 2010 +0200
+++ b/src/HOL/UNITY/WFair.thy	Thu Jul 22 18:08:39 2010 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/UNITY/WFair
+(*  Title:      HOL/UNITY/WFair.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1998  University of Cambridge
 
--- a/src/ZF/UNITY/MultisetSum.thy	Thu Jul 22 17:26:31 2010 +0200
+++ b/src/ZF/UNITY/MultisetSum.thy	Thu Jul 22 18:08:39 2010 +0200
@@ -1,4 +1,4 @@
-(*  Title:      ZF/UNITY/MultusetSum.thy
+(*  Title:      ZF/UNITY/MultisetSum.thy
     Author:     Sidi O Ehmety
 *)
 
--- a/src/ZF/UNITY/State.thy	Thu Jul 22 17:26:31 2010 +0200
+++ b/src/ZF/UNITY/State.thy	Thu Jul 22 18:08:39 2010 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/UNITY/State.thy
+(*  Title:      ZF/UNITY/State.thy
     Author:     Sidi O Ehmety, Computer Laboratory
     Copyright   2001  University of Cambridge
 
--- a/src/ZF/UNITY/WFair.thy	Thu Jul 22 17:26:31 2010 +0200
+++ b/src/ZF/UNITY/WFair.thy	Thu Jul 22 18:08:39 2010 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/UNITY/WFair.thy
+(*  Title:      ZF/UNITY/WFair.thy
     Author:     Sidi Ehmety, Computer Laboratory
     Copyright   1998  University of Cambridge
 *)
isabelle