updated some headers;
authorwenzelm
Thu Jul 22 18:08:39 2010 +0200 (2010-07-22)
changeset 379361e4c5015a72e
parent 37935 7551769de556
child 37937 9e482a3e651e
child 37945 32f9b7a70fc0
updated some headers;
src/HOL/Auth/CertifiedEmail.thy
src/HOL/Auth/Event.thy
src/HOL/Auth/KerberosIV.thy
src/HOL/Auth/KerberosIV_Gets.thy
src/HOL/Auth/KerberosV.thy
src/HOL/Auth/Kerberos_BAN.thy
src/HOL/Auth/Kerberos_BAN_Gets.thy
src/HOL/Auth/Message.thy
src/HOL/Auth/NS_Public.thy
src/HOL/Auth/NS_Public_Bad.thy
src/HOL/Auth/NS_Shared.thy
src/HOL/Auth/OtwayRees.thy
src/HOL/Auth/OtwayReesBella.thy
src/HOL/Auth/OtwayRees_AN.thy
src/HOL/Auth/OtwayRees_Bad.thy
src/HOL/Auth/Public.thy
src/HOL/Auth/Recur.thy
src/HOL/Auth/Shared.thy
src/HOL/Auth/TLS.thy
src/HOL/Auth/WooLam.thy
src/HOL/Auth/Yahalom.thy
src/HOL/Auth/Yahalom2.thy
src/HOL/Auth/Yahalom_Bad.thy
src/HOL/Auth/ZhouGollmann.thy
src/HOL/UNITY/Comp/Alloc.thy
src/HOL/UNITY/Comp/Handshake.thy
src/HOL/UNITY/Comp/Priority.thy
src/HOL/UNITY/Comp/PriorityAux.thy
src/HOL/UNITY/Comp/Progress.thy
src/HOL/UNITY/Comp/TimerArray.thy
src/HOL/UNITY/Detects.thy
src/HOL/UNITY/FP.thy
src/HOL/UNITY/Rename.thy
src/HOL/UNITY/Simple/Channel.thy
src/HOL/UNITY/Simple/Common.thy
src/HOL/UNITY/Simple/Deadlock.thy
src/HOL/UNITY/Simple/Lift.thy
src/HOL/UNITY/Simple/Mutex.thy
src/HOL/UNITY/Simple/NSP_Bad.thy
src/HOL/UNITY/Simple/Network.thy
src/HOL/UNITY/Simple/Reach.thy
src/HOL/UNITY/Simple/Reachability.thy
src/HOL/UNITY/Simple/Token.thy
src/HOL/UNITY/SubstAx.thy
src/HOL/UNITY/Transformers.thy
src/HOL/UNITY/UNITY_tactics.ML
src/HOL/UNITY/WFair.thy
src/ZF/UNITY/MultisetSum.thy
src/ZF/UNITY/State.thy
src/ZF/UNITY/WFair.thy
     1.1 --- a/src/HOL/Auth/CertifiedEmail.thy	Thu Jul 22 17:26:31 2010 +0200
     1.2 +++ b/src/HOL/Auth/CertifiedEmail.thy	Thu Jul 22 18:08:39 2010 +0200
     1.3 @@ -1,5 +1,4 @@
     1.4 -(*  Title:      HOL/Auth/CertifiedEmail
     1.5 -    ID:         $Id$
     1.6 +(*  Title:      HOL/Auth/CertifiedEmail.thy
     1.7      Author:     Giampaolo Bella, Christiano Longo and Lawrence C Paulson
     1.8  *)
     1.9  
     2.1 --- a/src/HOL/Auth/Event.thy	Thu Jul 22 17:26:31 2010 +0200
     2.2 +++ b/src/HOL/Auth/Event.thy	Thu Jul 22 18:08:39 2010 +0200
     2.3 @@ -1,5 +1,4 @@
     2.4 -(*  Title:      HOL/Auth/Event
     2.5 -    ID:         $Id$
     2.6 +(*  Title:      HOL/Auth/Event.thy
     2.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2.8      Copyright   1996  University of Cambridge
     2.9  
     3.1 --- a/src/HOL/Auth/KerberosIV.thy	Thu Jul 22 17:26:31 2010 +0200
     3.2 +++ b/src/HOL/Auth/KerberosIV.thy	Thu Jul 22 18:08:39 2010 +0200
     3.3 @@ -1,5 +1,4 @@
     3.4 -(*  Title:      HOL/Auth/KerberosIV
     3.5 -    ID:         $Id$
     3.6 +(*  Title:      HOL/Auth/KerberosIV.thy
     3.7      Author:     Giampaolo Bella, Cambridge University Computer Laboratory
     3.8      Copyright   1998  University of Cambridge
     3.9  *)
     4.1 --- a/src/HOL/Auth/KerberosIV_Gets.thy	Thu Jul 22 17:26:31 2010 +0200
     4.2 +++ b/src/HOL/Auth/KerberosIV_Gets.thy	Thu Jul 22 18:08:39 2010 +0200
     4.3 @@ -1,5 +1,4 @@
     4.4 -(*  Title:      HOL/Auth/KerberosIV
     4.5 -    ID:         $Id$
     4.6 +(*  Title:      HOL/Auth/KerberosIV_Gets.thy
     4.7      Author:     Giampaolo Bella, Cambridge University Computer Laboratory
     4.8      Copyright   1998  University of Cambridge
     4.9  *)
     5.1 --- a/src/HOL/Auth/KerberosV.thy	Thu Jul 22 17:26:31 2010 +0200
     5.2 +++ b/src/HOL/Auth/KerberosV.thy	Thu Jul 22 18:08:39 2010 +0200
     5.3 @@ -1,4 +1,4 @@
     5.4 -(*  ID:         $Id$
     5.5 +(*  Title:      HOL/Auth/KerberosV.thy
     5.6      Author:     Giampaolo Bella, Catania University
     5.7  *)
     5.8  
     6.1 --- a/src/HOL/Auth/Kerberos_BAN.thy	Thu Jul 22 17:26:31 2010 +0200
     6.2 +++ b/src/HOL/Auth/Kerberos_BAN.thy	Thu Jul 22 18:08:39 2010 +0200
     6.3 @@ -1,5 +1,4 @@
     6.4 -(*  Title:      HOL/Auth/Kerberos_BAN
     6.5 -    ID:         $Id$
     6.6 +(*  Title:      HOL/Auth/Kerberos_BAN.thy
     6.7      Author:     Giampaolo Bella, Cambridge University Computer Laboratory
     6.8      Copyright   1998  University of Cambridge
     6.9  *)
     7.1 --- a/src/HOL/Auth/Kerberos_BAN_Gets.thy	Thu Jul 22 17:26:31 2010 +0200
     7.2 +++ b/src/HOL/Auth/Kerberos_BAN_Gets.thy	Thu Jul 22 18:08:39 2010 +0200
     7.3 @@ -1,4 +1,4 @@
     7.4 -(*  ID:         $Id$
     7.5 +(*  Title:      HOL/Auth/Kerberos_BAN_Gets.thy
     7.6      Author:     Giampaolo Bella, Catania University
     7.7  *)
     7.8  
     8.1 --- a/src/HOL/Auth/Message.thy	Thu Jul 22 17:26:31 2010 +0200
     8.2 +++ b/src/HOL/Auth/Message.thy	Thu Jul 22 18:08:39 2010 +0200
     8.3 @@ -1,4 +1,4 @@
     8.4 -(*  Title:      HOL/Auth/Message
     8.5 +(*  Title:      HOL/Auth/Message.thy
     8.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     8.7      Copyright   1996  University of Cambridge
     8.8  
     9.1 --- a/src/HOL/Auth/NS_Public.thy	Thu Jul 22 17:26:31 2010 +0200
     9.2 +++ b/src/HOL/Auth/NS_Public.thy	Thu Jul 22 18:08:39 2010 +0200
     9.3 @@ -1,5 +1,4 @@
     9.4 -(*  Title:      HOL/Auth/NS_Public
     9.5 -    ID:         $Id$
     9.6 +(*  Title:      HOL/Auth/NS_Public.thy
     9.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     9.8      Copyright   1996  University of Cambridge
     9.9  
    10.1 --- a/src/HOL/Auth/NS_Public_Bad.thy	Thu Jul 22 17:26:31 2010 +0200
    10.2 +++ b/src/HOL/Auth/NS_Public_Bad.thy	Thu Jul 22 18:08:39 2010 +0200
    10.3 @@ -1,5 +1,4 @@
    10.4 -(*  Title:      HOL/Auth/NS_Public_Bad
    10.5 -    ID:         $Id$
    10.6 +(*  Title:      HOL/Auth/NS_Public_Bad.thy
    10.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    10.8      Copyright   1996  University of Cambridge
    10.9  
    11.1 --- a/src/HOL/Auth/NS_Shared.thy	Thu Jul 22 17:26:31 2010 +0200
    11.2 +++ b/src/HOL/Auth/NS_Shared.thy	Thu Jul 22 18:08:39 2010 +0200
    11.3 @@ -1,5 +1,4 @@
    11.4 -(*  Title:      HOL/Auth/NS_Shared
    11.5 -    ID:         $Id$
    11.6 +(*  Title:      HOL/Auth/NS_Shared.thy
    11.7      Author:     Lawrence C Paulson and Giampaolo Bella 
    11.8      Copyright   1996  University of Cambridge
    11.9  *)
    12.1 --- a/src/HOL/Auth/OtwayRees.thy	Thu Jul 22 17:26:31 2010 +0200
    12.2 +++ b/src/HOL/Auth/OtwayRees.thy	Thu Jul 22 18:08:39 2010 +0200
    12.3 @@ -1,5 +1,4 @@
    12.4 -(*  Title:      HOL/Auth/OtwayRees
    12.5 -    ID:         $Id$
    12.6 +(*  Title:      HOL/Auth/OtwayRees.thy
    12.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    12.8      Copyright   1996  University of Cambridge
    12.9  *)
    13.1 --- a/src/HOL/Auth/OtwayReesBella.thy	Thu Jul 22 17:26:31 2010 +0200
    13.2 +++ b/src/HOL/Auth/OtwayReesBella.thy	Thu Jul 22 18:08:39 2010 +0200
    13.3 @@ -1,4 +1,4 @@
    13.4 -(*  ID:         $Id$
    13.5 +(*  Title:      HOL/Auth/OtwayReesBella.thy
    13.6      Author:     Giampaolo Bella, Catania University
    13.7  *)
    13.8  
    14.1 --- a/src/HOL/Auth/OtwayRees_AN.thy	Thu Jul 22 17:26:31 2010 +0200
    14.2 +++ b/src/HOL/Auth/OtwayRees_AN.thy	Thu Jul 22 18:08:39 2010 +0200
    14.3 @@ -1,5 +1,4 @@
    14.4 -(*  Title:      HOL/Auth/OtwayRees
    14.5 -    ID:         $Id$
    14.6 +(*  Title:      HOL/Auth/OtwayRees_AN.thy
    14.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    14.8      Copyright   1996  University of Cambridge
    14.9  *)
    15.1 --- a/src/HOL/Auth/OtwayRees_Bad.thy	Thu Jul 22 17:26:31 2010 +0200
    15.2 +++ b/src/HOL/Auth/OtwayRees_Bad.thy	Thu Jul 22 18:08:39 2010 +0200
    15.3 @@ -1,5 +1,4 @@
    15.4 -(*  Title:      HOL/Auth/OtwayRees_Bad
    15.5 -    ID:         $Id$
    15.6 +(*  Title:      HOL/Auth/OtwayRees_Bad.thy
    15.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    15.8      Copyright   1996  University of Cambridge
    15.9  *)
    16.1 --- a/src/HOL/Auth/Public.thy	Thu Jul 22 17:26:31 2010 +0200
    16.2 +++ b/src/HOL/Auth/Public.thy	Thu Jul 22 18:08:39 2010 +0200
    16.3 @@ -1,4 +1,4 @@
    16.4 -(*  Title:      HOL/Auth/Public
    16.5 +(*  Title:      HOL/Auth/Public.thy
    16.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    16.7      Copyright   1996  University of Cambridge
    16.8  
    17.1 --- a/src/HOL/Auth/Recur.thy	Thu Jul 22 17:26:31 2010 +0200
    17.2 +++ b/src/HOL/Auth/Recur.thy	Thu Jul 22 18:08:39 2010 +0200
    17.3 @@ -1,5 +1,4 @@
    17.4 -(*  Title:      HOL/Auth/Recur
    17.5 -    ID:         $Id$
    17.6 +(*  Title:      HOL/Auth/Recur.thy
    17.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    17.8      Copyright   1996  University of Cambridge
    17.9  *)
    18.1 --- a/src/HOL/Auth/Shared.thy	Thu Jul 22 17:26:31 2010 +0200
    18.2 +++ b/src/HOL/Auth/Shared.thy	Thu Jul 22 18:08:39 2010 +0200
    18.3 @@ -1,4 +1,4 @@
    18.4 -(*  Title:      HOL/Auth/Shared
    18.5 +(*  Title:      HOL/Auth/Shared.thy
    18.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    18.7      Copyright   1996  University of Cambridge
    18.8  
    19.1 --- a/src/HOL/Auth/TLS.thy	Thu Jul 22 17:26:31 2010 +0200
    19.2 +++ b/src/HOL/Auth/TLS.thy	Thu Jul 22 18:08:39 2010 +0200
    19.3 @@ -1,5 +1,4 @@
    19.4 -(*  Title:      HOL/Auth/TLS
    19.5 -    ID:         $Id$
    19.6 +(*  Title:      HOL/Auth/TLS.thy
    19.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    19.8      Copyright   1997  University of Cambridge
    19.9  
    20.1 --- a/src/HOL/Auth/WooLam.thy	Thu Jul 22 17:26:31 2010 +0200
    20.2 +++ b/src/HOL/Auth/WooLam.thy	Thu Jul 22 18:08:39 2010 +0200
    20.3 @@ -1,5 +1,4 @@
    20.4 -(*  Title:      HOL/Auth/WooLam
    20.5 -    ID:         $Id$
    20.6 +(*  Title:      HOL/Auth/WooLam.thy
    20.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    20.8      Copyright   1996  University of Cambridge
    20.9  *)
    21.1 --- a/src/HOL/Auth/Yahalom.thy	Thu Jul 22 17:26:31 2010 +0200
    21.2 +++ b/src/HOL/Auth/Yahalom.thy	Thu Jul 22 18:08:39 2010 +0200
    21.3 @@ -1,5 +1,4 @@
    21.4 -(*  Title:      HOL/Auth/Yahalom
    21.5 -    ID:         $Id$
    21.6 +(*  Title:      HOL/Auth/Yahalom.thy
    21.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    21.8      Copyright   1996  University of Cambridge
    21.9  *)
    22.1 --- a/src/HOL/Auth/Yahalom2.thy	Thu Jul 22 17:26:31 2010 +0200
    22.2 +++ b/src/HOL/Auth/Yahalom2.thy	Thu Jul 22 18:08:39 2010 +0200
    22.3 @@ -1,5 +1,4 @@
    22.4 -(*  Title:      HOL/Auth/Yahalom2
    22.5 -    ID:         $Id$
    22.6 +(*  Title:      HOL/Auth/Yahalom2.thy
    22.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    22.8      Copyright   1996  University of Cambridge
    22.9  *)
    23.1 --- a/src/HOL/Auth/Yahalom_Bad.thy	Thu Jul 22 17:26:31 2010 +0200
    23.2 +++ b/src/HOL/Auth/Yahalom_Bad.thy	Thu Jul 22 18:08:39 2010 +0200
    23.3 @@ -1,5 +1,4 @@
    23.4 -(*  Title:      HOL/Auth/Yahalom
    23.5 -    ID:         $Id$
    23.6 +(*  Title:      HOL/Auth/Yahalom_Bad.thy
    23.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    23.8      Copyright   1996  University of Cambridge
    23.9  *)
    24.1 --- a/src/HOL/Auth/ZhouGollmann.thy	Thu Jul 22 17:26:31 2010 +0200
    24.2 +++ b/src/HOL/Auth/ZhouGollmann.thy	Thu Jul 22 18:08:39 2010 +0200
    24.3 @@ -1,5 +1,4 @@
    24.4 -(*  Title:      HOL/Auth/ZhouGollmann
    24.5 -    ID:         $Id$
    24.6 +(*  Title:      HOL/Auth/ZhouGollmann.thy
    24.7      Author:     Giampaolo Bella and L C Paulson, Cambridge Univ Computer Lab
    24.8      Copyright   2003  University of Cambridge
    24.9  
    25.1 --- a/src/HOL/UNITY/Comp/Alloc.thy	Thu Jul 22 17:26:31 2010 +0200
    25.2 +++ b/src/HOL/UNITY/Comp/Alloc.thy	Thu Jul 22 18:08:39 2010 +0200
    25.3 @@ -1,4 +1,4 @@
    25.4 -(*  ID:         $Id$
    25.5 +(*  Title:      HOL/UNITY/Comp/Alloc.thy
    25.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    25.7      Copyright   1998  University of Cambridge
    25.8  
    26.1 --- a/src/HOL/UNITY/Comp/Handshake.thy	Thu Jul 22 17:26:31 2010 +0200
    26.2 +++ b/src/HOL/UNITY/Comp/Handshake.thy	Thu Jul 22 18:08:39 2010 +0200
    26.3 @@ -1,5 +1,4 @@
    26.4 -(*  Title:      HOL/UNITY/Handshake.thy
    26.5 -    ID:         $Id$
    26.6 +(*  Title:      HOL/UNITY/Comp/Handshake.thy
    26.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    26.8      Copyright   1998  University of Cambridge
    26.9  
    27.1 --- a/src/HOL/UNITY/Comp/Priority.thy	Thu Jul 22 17:26:31 2010 +0200
    27.2 +++ b/src/HOL/UNITY/Comp/Priority.thy	Thu Jul 22 18:08:39 2010 +0200
    27.3 @@ -1,4 +1,4 @@
    27.4 -(*  Title:      HOL/UNITY/Priority
    27.5 +(*  Title:      HOL/UNITY/Comp/Priority.thy
    27.6      Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
    27.7      Copyright   2001  University of Cambridge
    27.8  *)
    28.1 --- a/src/HOL/UNITY/Comp/PriorityAux.thy	Thu Jul 22 17:26:31 2010 +0200
    28.2 +++ b/src/HOL/UNITY/Comp/PriorityAux.thy	Thu Jul 22 18:08:39 2010 +0200
    28.3 @@ -1,5 +1,4 @@
    28.4 -(*  Title:      HOL/UNITY/PriorityAux
    28.5 -    ID:         $Id$
    28.6 +(*  Title:      HOL/UNITY/Comp/PriorityAux.thy
    28.7      Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
    28.8      Copyright   2001  University of Cambridge
    28.9  
    29.1 --- a/src/HOL/UNITY/Comp/Progress.thy	Thu Jul 22 17:26:31 2010 +0200
    29.2 +++ b/src/HOL/UNITY/Comp/Progress.thy	Thu Jul 22 18:08:39 2010 +0200
    29.3 @@ -1,4 +1,4 @@
    29.4 -(*  Title:      HOL/UNITY/Progress
    29.5 +(*  Title:      HOL/UNITY/Comp/Progress.thy
    29.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    29.7      Copyright   2003  University of Cambridge
    29.8  
    30.1 --- a/src/HOL/UNITY/Comp/TimerArray.thy	Thu Jul 22 17:26:31 2010 +0200
    30.2 +++ b/src/HOL/UNITY/Comp/TimerArray.thy	Thu Jul 22 18:08:39 2010 +0200
    30.3 @@ -1,4 +1,4 @@
    30.4 -(*  Title:      HOL/UNITY/TimerArray.thy
    30.5 +(*  Title:      HOL/UNITY/Comp/TimerArray.thy
    30.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    30.7      Copyright   1998  University of Cambridge
    30.8  
    31.1 --- a/src/HOL/UNITY/Detects.thy	Thu Jul 22 17:26:31 2010 +0200
    31.2 +++ b/src/HOL/UNITY/Detects.thy	Thu Jul 22 18:08:39 2010 +0200
    31.3 @@ -1,5 +1,4 @@
    31.4 -(*  Title:      HOL/UNITY/Detects
    31.5 -    ID:         $Id$
    31.6 +(*  Title:      HOL/UNITY/Detects.thy
    31.7      Author:     Tanja Vos, Cambridge University Computer Laboratory
    31.8      Copyright   2000  University of Cambridge
    31.9  
    32.1 --- a/src/HOL/UNITY/FP.thy	Thu Jul 22 17:26:31 2010 +0200
    32.2 +++ b/src/HOL/UNITY/FP.thy	Thu Jul 22 18:08:39 2010 +0200
    32.3 @@ -1,4 +1,4 @@
    32.4 -(*  Title:      HOL/UNITY/FP
    32.5 +(*  Title:      HOL/UNITY/FP.thy
    32.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    32.7      Copyright   1998  University of Cambridge
    32.8  
    33.1 --- a/src/HOL/UNITY/Rename.thy	Thu Jul 22 17:26:31 2010 +0200
    33.2 +++ b/src/HOL/UNITY/Rename.thy	Thu Jul 22 18:08:39 2010 +0200
    33.3 @@ -1,5 +1,4 @@
    33.4  (*  Title:      HOL/UNITY/Rename.thy
    33.5 -    ID:         $Id$
    33.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    33.7      Copyright   2000  University of Cambridge
    33.8  *)
    34.1 --- a/src/HOL/UNITY/Simple/Channel.thy	Thu Jul 22 17:26:31 2010 +0200
    34.2 +++ b/src/HOL/UNITY/Simple/Channel.thy	Thu Jul 22 18:08:39 2010 +0200
    34.3 @@ -1,5 +1,4 @@
    34.4 -(*  Title:      HOL/UNITY/Channel
    34.5 -    ID:         $Id$
    34.6 +(*  Title:      HOL/UNITY/Simple/Channel.thy
    34.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    34.8      Copyright   1998  University of Cambridge
    34.9  
    35.1 --- a/src/HOL/UNITY/Simple/Common.thy	Thu Jul 22 17:26:31 2010 +0200
    35.2 +++ b/src/HOL/UNITY/Simple/Common.thy	Thu Jul 22 18:08:39 2010 +0200
    35.3 @@ -1,4 +1,4 @@
    35.4 -(*  Title:      HOL/UNITY/Common
    35.5 +(*  Title:      HOL/UNITY/Simple/Common.thy
    35.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    35.7      Copyright   1998  University of Cambridge
    35.8  
    36.1 --- a/src/HOL/UNITY/Simple/Deadlock.thy	Thu Jul 22 17:26:31 2010 +0200
    36.2 +++ b/src/HOL/UNITY/Simple/Deadlock.thy	Thu Jul 22 18:08:39 2010 +0200
    36.3 @@ -1,4 +1,4 @@
    36.4 -(*  Title:      HOL/UNITY/Deadlock.thy
    36.5 +(*  Title:      HOL/UNITY/Simple/Deadlock.thy
    36.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    36.7      Copyright   1998  University of Cambridge
    36.8  
    37.1 --- a/src/HOL/UNITY/Simple/Lift.thy	Thu Jul 22 17:26:31 2010 +0200
    37.2 +++ b/src/HOL/UNITY/Simple/Lift.thy	Thu Jul 22 18:08:39 2010 +0200
    37.3 @@ -1,4 +1,4 @@
    37.4 -(*  Title:      HOL/UNITY/Lift.thy
    37.5 +(*  Title:      HOL/UNITY/Simple/Lift.thy
    37.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    37.7      Copyright   1998  University of Cambridge
    37.8  
    38.1 --- a/src/HOL/UNITY/Simple/Mutex.thy	Thu Jul 22 17:26:31 2010 +0200
    38.2 +++ b/src/HOL/UNITY/Simple/Mutex.thy	Thu Jul 22 18:08:39 2010 +0200
    38.3 @@ -1,4 +1,4 @@
    38.4 -(*  Title:      HOL/UNITY/Mutex.thy
    38.5 +(*  Title:      HOL/UNITY/Simple/Mutex.thy
    38.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    38.7      Copyright   1998  University of Cambridge
    38.8  
    39.1 --- a/src/HOL/UNITY/Simple/NSP_Bad.thy	Thu Jul 22 17:26:31 2010 +0200
    39.2 +++ b/src/HOL/UNITY/Simple/NSP_Bad.thy	Thu Jul 22 18:08:39 2010 +0200
    39.3 @@ -1,4 +1,4 @@
    39.4 -(*  Title:      HOL/Auth/NSP_Bad.thy
    39.5 +(*  Title:      HOL/UNITY/Simple/NSP_Bad.thy
    39.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    39.7      Copyright   1996  University of Cambridge
    39.8  
    40.1 --- a/src/HOL/UNITY/Simple/Network.thy	Thu Jul 22 17:26:31 2010 +0200
    40.2 +++ b/src/HOL/UNITY/Simple/Network.thy	Thu Jul 22 18:08:39 2010 +0200
    40.3 @@ -1,4 +1,4 @@
    40.4 -(*  Title:      HOL/UNITY/Network.thy
    40.5 +(*  Title:      HOL/UNITY/Simple/Network.thy
    40.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    40.7      Copyright   1998  University of Cambridge
    40.8  
    41.1 --- a/src/HOL/UNITY/Simple/Reach.thy	Thu Jul 22 17:26:31 2010 +0200
    41.2 +++ b/src/HOL/UNITY/Simple/Reach.thy	Thu Jul 22 18:08:39 2010 +0200
    41.3 @@ -1,4 +1,4 @@
    41.4 -(*  Title:      HOL/UNITY/Reach.thy
    41.5 +(*  Title:      HOL/UNITY/Simple/Reach.thy
    41.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    41.7      Copyright   1998  University of Cambridge
    41.8  
    42.1 --- a/src/HOL/UNITY/Simple/Reachability.thy	Thu Jul 22 17:26:31 2010 +0200
    42.2 +++ b/src/HOL/UNITY/Simple/Reachability.thy	Thu Jul 22 18:08:39 2010 +0200
    42.3 @@ -1,4 +1,4 @@
    42.4 -(*  Title:      HOL/UNITY/Reachability.thy
    42.5 +(*  Title:      HOL/UNITY/Simple/Reachability.thy
    42.6      Author:     Tanja Vos, Cambridge University Computer Laboratory
    42.7      Copyright   2000  University of Cambridge
    42.8  
    43.1 --- a/src/HOL/UNITY/Simple/Token.thy	Thu Jul 22 17:26:31 2010 +0200
    43.2 +++ b/src/HOL/UNITY/Simple/Token.thy	Thu Jul 22 18:08:39 2010 +0200
    43.3 @@ -1,4 +1,4 @@
    43.4 -(*  Title:      HOL/UNITY/Token
    43.5 +(*  Title:      HOL/UNITY/Simple/Token.thy
    43.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    43.7      Copyright   1998  University of Cambridge
    43.8  *)
    44.1 --- a/src/HOL/UNITY/SubstAx.thy	Thu Jul 22 17:26:31 2010 +0200
    44.2 +++ b/src/HOL/UNITY/SubstAx.thy	Thu Jul 22 18:08:39 2010 +0200
    44.3 @@ -1,4 +1,4 @@
    44.4 -(*  Title:      HOL/UNITY/SubstAx
    44.5 +(*  Title:      HOL/UNITY/SubstAx.thy
    44.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    44.7      Copyright   1998  University of Cambridge
    44.8  
    45.1 --- a/src/HOL/UNITY/Transformers.thy	Thu Jul 22 17:26:31 2010 +0200
    45.2 +++ b/src/HOL/UNITY/Transformers.thy	Thu Jul 22 18:08:39 2010 +0200
    45.3 @@ -1,4 +1,4 @@
    45.4 -(*  Title:      HOL/UNITY/Transformers
    45.5 +(*  Title:      HOL/UNITY/Transformers.thy
    45.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    45.7      Copyright   2003  University of Cambridge
    45.8  
    46.1 --- a/src/HOL/UNITY/UNITY_tactics.ML	Thu Jul 22 17:26:31 2010 +0200
    46.2 +++ b/src/HOL/UNITY/UNITY_tactics.ML	Thu Jul 22 18:08:39 2010 +0200
    46.3 @@ -1,5 +1,4 @@
    46.4  (*  Title:      HOL/UNITY/UNITY_tactics.ML
    46.5 -    ID:         $Id$
    46.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    46.7      Copyright   2003  University of Cambridge
    46.8  
    47.1 --- a/src/HOL/UNITY/WFair.thy	Thu Jul 22 17:26:31 2010 +0200
    47.2 +++ b/src/HOL/UNITY/WFair.thy	Thu Jul 22 18:08:39 2010 +0200
    47.3 @@ -1,4 +1,4 @@
    47.4 -(*  Title:      HOL/UNITY/WFair
    47.5 +(*  Title:      HOL/UNITY/WFair.thy
    47.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    47.7      Copyright   1998  University of Cambridge
    47.8  
    48.1 --- a/src/ZF/UNITY/MultisetSum.thy	Thu Jul 22 17:26:31 2010 +0200
    48.2 +++ b/src/ZF/UNITY/MultisetSum.thy	Thu Jul 22 18:08:39 2010 +0200
    48.3 @@ -1,4 +1,4 @@
    48.4 -(*  Title:      ZF/UNITY/MultusetSum.thy
    48.5 +(*  Title:      ZF/UNITY/MultisetSum.thy
    48.6      Author:     Sidi O Ehmety
    48.7  *)
    48.8  
    49.1 --- a/src/ZF/UNITY/State.thy	Thu Jul 22 17:26:31 2010 +0200
    49.2 +++ b/src/ZF/UNITY/State.thy	Thu Jul 22 18:08:39 2010 +0200
    49.3 @@ -1,4 +1,4 @@
    49.4 -(*  Title:      HOL/UNITY/State.thy
    49.5 +(*  Title:      ZF/UNITY/State.thy
    49.6      Author:     Sidi O Ehmety, Computer Laboratory
    49.7      Copyright   2001  University of Cambridge
    49.8  
    50.1 --- a/src/ZF/UNITY/WFair.thy	Thu Jul 22 17:26:31 2010 +0200
    50.2 +++ b/src/ZF/UNITY/WFair.thy	Thu Jul 22 18:08:39 2010 +0200
    50.3 @@ -1,4 +1,4 @@
    50.4 -(*  Title:      HOL/UNITY/WFair.thy
    50.5 +(*  Title:      ZF/UNITY/WFair.thy
    50.6      Author:     Sidi Ehmety, Computer Laboratory
    50.7      Copyright   1998  University of Cambridge
    50.8  *)