# HG changeset patch
# User wenzelm
# Date 1279814919 -7200
# Node ID 1e4c5015a72e39ea5cb0a44f75425a27c14c98f1
# Parent  7551769de556d4e0a9a74cfccd510da7262ccd72
updated some headers;

diff -r 7551769de556 -r 1e4c5015a72e src/HOL/Auth/CertifiedEmail.thy
--- 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
 *)
 
diff -r 7551769de556 -r 1e4c5015a72e src/HOL/Auth/Event.thy
--- 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
 
diff -r 7551769de556 -r 1e4c5015a72e src/HOL/Auth/KerberosIV.thy
--- 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
 *)
diff -r 7551769de556 -r 1e4c5015a72e src/HOL/Auth/KerberosIV_Gets.thy
--- 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
 *)
diff -r 7551769de556 -r 1e4c5015a72e src/HOL/Auth/KerberosV.thy
--- 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
 *)
 
diff -r 7551769de556 -r 1e4c5015a72e src/HOL/Auth/Kerberos_BAN.thy
--- 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
 *)
diff -r 7551769de556 -r 1e4c5015a72e src/HOL/Auth/Kerberos_BAN_Gets.thy
--- 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
 *)
 
diff -r 7551769de556 -r 1e4c5015a72e src/HOL/Auth/Message.thy
--- 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
 
diff -r 7551769de556 -r 1e4c5015a72e src/HOL/Auth/NS_Public.thy
--- 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
 
diff -r 7551769de556 -r 1e4c5015a72e src/HOL/Auth/NS_Public_Bad.thy
--- 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
 
diff -r 7551769de556 -r 1e4c5015a72e src/HOL/Auth/NS_Shared.thy
--- 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
 *)
diff -r 7551769de556 -r 1e4c5015a72e src/HOL/Auth/OtwayRees.thy
--- 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
 *)
diff -r 7551769de556 -r 1e4c5015a72e src/HOL/Auth/OtwayReesBella.thy
--- 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
 *)
 
diff -r 7551769de556 -r 1e4c5015a72e src/HOL/Auth/OtwayRees_AN.thy
--- 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
 *)
diff -r 7551769de556 -r 1e4c5015a72e src/HOL/Auth/OtwayRees_Bad.thy
--- 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
 *)
diff -r 7551769de556 -r 1e4c5015a72e src/HOL/Auth/Public.thy
--- 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
 
diff -r 7551769de556 -r 1e4c5015a72e src/HOL/Auth/Recur.thy
--- 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
 *)
diff -r 7551769de556 -r 1e4c5015a72e src/HOL/Auth/Shared.thy
--- 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
 
diff -r 7551769de556 -r 1e4c5015a72e src/HOL/Auth/TLS.thy
--- 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
 
diff -r 7551769de556 -r 1e4c5015a72e src/HOL/Auth/WooLam.thy
--- 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
 *)
diff -r 7551769de556 -r 1e4c5015a72e src/HOL/Auth/Yahalom.thy
--- 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
 *)
diff -r 7551769de556 -r 1e4c5015a72e src/HOL/Auth/Yahalom2.thy
--- 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
 *)
diff -r 7551769de556 -r 1e4c5015a72e src/HOL/Auth/Yahalom_Bad.thy
--- 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
 *)
diff -r 7551769de556 -r 1e4c5015a72e src/HOL/Auth/ZhouGollmann.thy
--- 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
 
diff -r 7551769de556 -r 1e4c5015a72e src/HOL/UNITY/Comp/Alloc.thy
--- 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
 
diff -r 7551769de556 -r 1e4c5015a72e src/HOL/UNITY/Comp/Handshake.thy
--- 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
 
diff -r 7551769de556 -r 1e4c5015a72e src/HOL/UNITY/Comp/Priority.thy
--- 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
 *)
diff -r 7551769de556 -r 1e4c5015a72e src/HOL/UNITY/Comp/PriorityAux.thy
--- 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
 
diff -r 7551769de556 -r 1e4c5015a72e src/HOL/UNITY/Comp/Progress.thy
--- 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
 
diff -r 7551769de556 -r 1e4c5015a72e src/HOL/UNITY/Comp/TimerArray.thy
--- 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
 
diff -r 7551769de556 -r 1e4c5015a72e src/HOL/UNITY/Detects.thy
--- 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
 
diff -r 7551769de556 -r 1e4c5015a72e src/HOL/UNITY/FP.thy
--- 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
 
diff -r 7551769de556 -r 1e4c5015a72e src/HOL/UNITY/Rename.thy
--- 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
 *)
diff -r 7551769de556 -r 1e4c5015a72e src/HOL/UNITY/Simple/Channel.thy
--- 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
 
diff -r 7551769de556 -r 1e4c5015a72e src/HOL/UNITY/Simple/Common.thy
--- 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
 
diff -r 7551769de556 -r 1e4c5015a72e src/HOL/UNITY/Simple/Deadlock.thy
--- 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
 
diff -r 7551769de556 -r 1e4c5015a72e src/HOL/UNITY/Simple/Lift.thy
--- 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
 
diff -r 7551769de556 -r 1e4c5015a72e src/HOL/UNITY/Simple/Mutex.thy
--- 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
 
diff -r 7551769de556 -r 1e4c5015a72e src/HOL/UNITY/Simple/NSP_Bad.thy
--- 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
 
diff -r 7551769de556 -r 1e4c5015a72e src/HOL/UNITY/Simple/Network.thy
--- 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
 
diff -r 7551769de556 -r 1e4c5015a72e src/HOL/UNITY/Simple/Reach.thy
--- 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
 
diff -r 7551769de556 -r 1e4c5015a72e src/HOL/UNITY/Simple/Reachability.thy
--- 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
 
diff -r 7551769de556 -r 1e4c5015a72e src/HOL/UNITY/Simple/Token.thy
--- 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
 *)
diff -r 7551769de556 -r 1e4c5015a72e src/HOL/UNITY/SubstAx.thy
--- 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
 
diff -r 7551769de556 -r 1e4c5015a72e src/HOL/UNITY/Transformers.thy
--- 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
 
diff -r 7551769de556 -r 1e4c5015a72e src/HOL/UNITY/UNITY_tactics.ML
--- 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
 
diff -r 7551769de556 -r 1e4c5015a72e src/HOL/UNITY/WFair.thy
--- 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
 
diff -r 7551769de556 -r 1e4c5015a72e src/ZF/UNITY/MultisetSum.thy
--- 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
 *)
 
diff -r 7551769de556 -r 1e4c5015a72e src/ZF/UNITY/State.thy
--- 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
 
diff -r 7551769de556 -r 1e4c5015a72e src/ZF/UNITY/WFair.thy
--- 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
 *)