tuned headers;

--- a/src/HOL/HOLCF/Bifinite.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/Bifinite.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/Bifinite.thy
+(*  Title:      HOL/HOLCF/Bifinite.thy
     Author:     Brian Huffman
 *)
 

--- a/src/HOL/HOLCF/Cfun.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/Cfun.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/Cfun.thy
+(*  Title:      HOL/HOLCF/Cfun.thy
     Author:     Franz Regensburger
     Author:     Brian Huffman
 *)

--- a/src/HOL/HOLCF/Compact_Basis.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/Compact_Basis.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/Compact_Basis.thy
+(*  Title:      HOL/HOLCF/Compact_Basis.thy
     Author:     Brian Huffman
 *)
 

--- a/src/HOL/HOLCF/Completion.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/Completion.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/Completion.thy
+(*  Title:      HOL/HOLCF/Completion.thy
     Author:     Brian Huffman
 *)
 

--- a/src/HOL/HOLCF/Cont.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/Cont.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/Cont.thy
+(*  Title:      HOL/HOLCF/Cont.thy
     Author:     Franz Regensburger
     Author:     Brian Huffman
 *)

--- a/src/HOL/HOLCF/ConvexPD.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/ConvexPD.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/ConvexPD.thy
+(*  Title:      HOL/HOLCF/ConvexPD.thy
     Author:     Brian Huffman
 *)
 

--- a/src/HOL/HOLCF/Cpodef.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/Cpodef.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/Pcpodef.thy
+(*  Title:      HOL/HOLCF/Cpodef.thy
     Author:     Brian Huffman
 *)
 

--- a/src/HOL/HOLCF/Cprod.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/Cprod.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/Cprod.thy
+(*  Title:      HOL/HOLCF/Cprod.thy
     Author:     Franz Regensburger
 *)
 

--- a/src/HOL/HOLCF/Deflation.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/Deflation.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/Deflation.thy
+(*  Title:      HOL/HOLCF/Deflation.thy
     Author:     Brian Huffman
 *)
 

--- a/src/HOL/HOLCF/Discrete.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/Discrete.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/Discrete.thy
+(*  Title:      HOL/HOLCF/Discrete.thy
     Author:     Tobias Nipkow
 *)
 

--- a/src/HOL/HOLCF/Domain.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/Domain.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/Domain.thy
+(*  Title:      HOL/HOLCF/Domain.thy
     Author:     Brian Huffman
 *)
 

--- a/src/HOL/HOLCF/Domain_Aux.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/Domain_Aux.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/Domain_Aux.thy
+(*  Title:      HOL/HOLCF/Domain_Aux.thy
     Author:     Brian Huffman
 *)
 

--- a/src/HOL/HOLCF/FOCUS/Buffer.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/FOCUS/Buffer.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/FOCUS/Buffer.thy
+(*  Title:      HOL/HOLCF/FOCUS/Buffer.thy
     Author:     David von Oheimb, TU Muenchen
 
 Formalization of section 4 of

--- a/src/HOL/HOLCF/FOCUS/Buffer_adm.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/FOCUS/Buffer_adm.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/FOCUS/Buffer_adm.thy
+(*  Title:      HOL/HOLCF/FOCUS/Buffer_adm.thy
     Author:     David von Oheimb, TU Muenchen
 *)
 

--- a/src/HOL/HOLCF/FOCUS/FOCUS.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/FOCUS/FOCUS.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/FOCUS/FOCUS.thy
+(*  Title:      HOL/HOLCF/FOCUS/FOCUS.thy
     Author:     David von Oheimb, TU Muenchen
 *)
 

--- a/src/HOL/HOLCF/FOCUS/Fstream.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/FOCUS/Fstream.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/FOCUS/Fstream.thy
+(*  Title:      HOL/HOLCF/FOCUS/Fstream.thy
     Author:     David von Oheimb, TU Muenchen
 
 FOCUS streams (with lifted elements).

--- a/src/HOL/HOLCF/FOCUS/Fstreams.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/FOCUS/Fstreams.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/FOCUS/Fstreams.thy
+(*  Title:      HOL/HOLCF/FOCUS/Fstreams.thy
     Author:     Borislav Gajanovic
 
 FOCUS flat streams (with lifted elements).

--- a/src/HOL/HOLCF/FOCUS/Stream_adm.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/FOCUS/Stream_adm.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/ex/Stream_adm.thy
+(*  Title:      HOL/HOLCF/FOCUS/Stream_adm.thy
     Author:     David von Oheimb, TU Muenchen
 *)
 

--- a/src/HOL/HOLCF/Fix.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/Fix.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/Fix.thy
+(*  Title:      HOL/HOLCF/Fix.thy
     Author:     Franz Regensburger
     Author:     Brian Huffman
 *)

--- a/src/HOL/HOLCF/Fixrec.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/Fixrec.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/Fixrec.thy
+(*  Title:      HOL/HOLCF/Fixrec.thy
     Author:     Amber Telfer and Brian Huffman
 *)
 

--- a/src/HOL/HOLCF/Fun_Cpo.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/Fun_Cpo.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/Fun_Cpo.thy
+(*  Title:      HOL/HOLCF/Fun_Cpo.thy
     Author:     Franz Regensburger
     Author:     Brian Huffman
 *)

--- a/src/HOL/HOLCF/HOLCF.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/HOLCF.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/HOLCF.thy
+(*  Title:      HOL/HOLCF/HOLCF.thy
     Author:     Franz Regensburger
 
 HOLCF -- a semantic extension of HOL by the LCF logic.

--- a/src/HOL/HOLCF/IMP/Denotational.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/IMP/Denotational.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/IMP/Denotational.thy
+(*  Title:      HOL/HOLCF/IMP/Denotational.thy
     Author:     Tobias Nipkow and Robert Sandner, TUM
     Copyright   1996 TUM
 *)

--- a/src/HOL/HOLCF/IMP/HoareEx.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/IMP/HoareEx.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/IMP/HoareEx.thy
+(*  Title:      HOL/HOLCF/IMP/HoareEx.thy
     Author:     Tobias Nipkow, TUM
     Copyright   1997 TUM
 *)

--- a/src/HOL/HOLCF/IOA/ABP/Abschannel.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/IOA/ABP/Abschannel.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/IOA/ABP/Abschannel.thy
+(*  Title:      HOL/HOLCF/IOA/ABP/Abschannel.thy
     Author:     Olaf Müller
 *)
 

--- a/src/HOL/HOLCF/IOA/ABP/Abschannel_finite.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/IOA/ABP/Abschannel_finite.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/IOA/ABP/Abschannels.thy
+(*  Title:      HOL/HOLCF/IOA/ABP/Abschannel_finite.thy
     Author:     Olaf Müller
 *)
 

--- a/src/HOL/HOLCF/IOA/ABP/Action.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/IOA/ABP/Action.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/IOA/ABP/Action.thy
+(*  Title:      HOL/HOLCF/IOA/ABP/Action.thy
     Author:     Olaf Müller
 *)
 

--- a/src/HOL/HOLCF/IOA/ABP/Check.ML	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/IOA/ABP/Check.ML	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/IOA/ABP/Check.ML
+(*  Title:      HOL/HOLCF/IOA/ABP/Check.ML
     Author:     Olaf Mueller
 
 The Model Checker.

--- a/src/HOL/HOLCF/IOA/ABP/Correctness.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/IOA/ABP/Correctness.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/IOA/ABP/Correctness.thy
+(*  Title:      HOL/HOLCF/IOA/ABP/Correctness.thy
     Author:     Olaf Müller
 *)
 

--- a/src/HOL/HOLCF/IOA/ABP/Env.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/IOA/ABP/Env.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/IOA/ABP/Impl.thy
+(*  Title:      HOL/HOLCF/IOA/ABP/Env.thy
     Author:     Olaf Müller
 *)
 

--- a/src/HOL/HOLCF/IOA/ABP/Impl.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/IOA/ABP/Impl.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/IOA/ABP/Impl.thy
+(*  Title:      HOL/HOLCF/IOA/ABP/Impl.thy
     Author:     Olaf Müller
 *)
 

--- a/src/HOL/HOLCF/IOA/ABP/Impl_finite.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/IOA/ABP/Impl_finite.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/IOA/ABP/Impl.thy
+(*  Title:      HOL/HOLCF/IOA/ABP/Impl_finite.thy
     Author:     Olaf Müller
 *)
 

--- a/src/HOL/HOLCF/IOA/ABP/Lemmas.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/IOA/ABP/Lemmas.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/IOA/ABP/Lemmas.thy
+(*  Title:      HOL/HOLCF/IOA/ABP/Lemmas.thy
     Author:     Olaf Müller
 *)
 

--- a/src/HOL/HOLCF/IOA/ABP/Packet.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/IOA/ABP/Packet.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/IOA/ABP/Packet.thy
+(*  Title:      HOL/HOLCF/IOA/ABP/Packet.thy
     Author:     Olaf Müller
 *)
 

--- a/src/HOL/HOLCF/IOA/ABP/ROOT.ML	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/IOA/ABP/ROOT.ML	Tue Mar 29 17:47:11 2011 +0200
@@ -1,7 +1,8 @@
-(*  Title:      HOLCF/IOA/ABP/ROOT.ML
+(*  Title:      HOL/HOLCF/IOA/ABP/ROOT.ML
     Author:     Olaf Mueller
 
 This is the ROOT file for the Alternating Bit Protocol performed in
 I/O-Automata.
 *)
+
 use_thys ["Correctness"];

--- a/src/HOL/HOLCF/IOA/ABP/Receiver.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/IOA/ABP/Receiver.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/IOA/ABP/Receiver.thy
+(*  Title:      HOL/HOLCF/IOA/ABP/Receiver.thy
     Author:     Olaf Müller
 *)
 

--- a/src/HOL/HOLCF/IOA/ABP/Sender.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/IOA/ABP/Sender.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/IOA/ABP/Sender.thy
+(*  Title:      HOL/HOLCF/IOA/ABP/Sender.thy
     Author:     Olaf Müller
 *)
 

--- a/src/HOL/HOLCF/IOA/ABP/Spec.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/IOA/ABP/Spec.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/IOA/ABP/Spec.thy
+(*  Title:      HOL/HOLCF/IOA/ABP/Spec.thy
     Author:     Olaf Müller
 *)
 

--- a/src/HOL/HOLCF/IOA/NTP/Abschannel.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/IOA/NTP/Abschannel.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/IOA/NTP/Abschannel.thy
+(*  Title:      HOL/HOLCF/IOA/NTP/Abschannel.thy
     Author:     Olaf Müller
 *)
 

--- a/src/HOL/HOLCF/IOA/NTP/Action.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/IOA/NTP/Action.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/IOA/NTP/Action.thy
+(*  Title:      HOL/HOLCF/IOA/NTP/Action.thy
     Author:     Tobias Nipkow & Konrad Slind
 *)
 

--- a/src/HOL/HOLCF/IOA/NTP/Correctness.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/IOA/NTP/Correctness.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/IOA/NTP/Correctness.thy
+(*  Title:      HOL/HOLCF/IOA/NTP/Correctness.thy
     Author:     Tobias Nipkow & Konrad Slind
 *)
 

--- a/src/HOL/HOLCF/IOA/NTP/Impl.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/IOA/NTP/Impl.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/IOA/NTP/Impl.thy
+(*  Title:      HOL/HOLCF/IOA/NTP/Impl.thy
     Author:     Tobias Nipkow & Konrad Slind
 *)
 

--- a/src/HOL/HOLCF/IOA/NTP/Lemmas.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/IOA/NTP/Lemmas.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/IOA/NTP/Lemmas.thy
+(*  Title:      HOL/HOLCF/IOA/NTP/Lemmas.thy
     Author:     Tobias Nipkow & Konrad Slind
 *)
 

--- a/src/HOL/HOLCF/IOA/NTP/Multiset.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/IOA/NTP/Multiset.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/IOA/NTP/Multiset.thy
+(*  Title:      HOL/HOLCF/IOA/NTP/Multiset.thy
     Author:     Tobias Nipkow & Konrad Slind
 *)
 

--- a/src/HOL/HOLCF/IOA/NTP/Packet.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/IOA/NTP/Packet.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/IOA/NTP/Packet.thy
+(*  Title:      HOL/HOLCF/IOA/NTP/Packet.thy
     Author:     Tobias Nipkow & Konrad Slind
 *)
 

--- a/src/HOL/HOLCF/IOA/NTP/ROOT.ML	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/IOA/NTP/ROOT.ML	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/IOA/NTP/ROOT.ML
+(*  Title:      HOL/HOLCF/IOA/NTP/ROOT.ML
     Author:     Tobias Nipkow & Konrad Slind
 
 This is the ROOT file for a network transmission protocol (NTP

--- a/src/HOL/HOLCF/IOA/NTP/Receiver.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/IOA/NTP/Receiver.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/IOA/NTP/Receiver.thy
+(*  Title:      HOL/HOLCF/IOA/NTP/Receiver.thy
     Author:     Tobias Nipkow & Konrad Slind
 *)
 

--- a/src/HOL/HOLCF/IOA/NTP/Sender.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/IOA/NTP/Sender.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/IOA/NTP/Sender.thy
+(*  Title:      HOL/HOLCF/IOA/NTP/Sender.thy
     Author:     Tobias Nipkow & Konrad Slind
 *)
 

--- a/src/HOL/HOLCF/IOA/NTP/Spec.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/IOA/NTP/Spec.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/IOA/NTP/Spec.thy
+(*  Title:      HOL/HOLCF/IOA/NTP/Spec.thy
     Author:     Tobias Nipkow & Konrad Slind
 *)
 

--- a/src/HOL/HOLCF/IOA/ROOT.ML	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/IOA/ROOT.ML	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/IOA/ROOT.ML
+(*  Title:      HOL/HOLCF/IOA/ROOT.ML
     Author:     Olaf Mueller
 
 Formalization of a semantic model of I/O-Automata.  See README.html

--- a/src/HOL/HOLCF/IOA/Storage/Action.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/IOA/Storage/Action.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/IOA/ABP/Action.thy
+(*  Title:      HOL/HOLCF/IOA/Storage/Action.thy
     Author:     Olaf Müller
 *)
 

--- a/src/HOL/HOLCF/IOA/Storage/Correctness.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/IOA/Storage/Correctness.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/IOA/example/Correctness.thy
+(*  Title:      HOL/HOLCF/IOA/Storage/Correctness.thy
     Author:     Olaf Müller
 *)
 

--- a/src/HOL/HOLCF/IOA/Storage/Impl.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/IOA/Storage/Impl.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/IOA/example/Spec.thy
+(*  Title:      HOL/HOLCF/IOA/Storage/Impl.thy
     Author:     Olaf Müller
 *)
 

--- a/src/HOL/HOLCF/IOA/Storage/ROOT.ML	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/IOA/Storage/ROOT.ML	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/IOA/Storage/ROOT.ML
+(*  Title:      HOL/HOLCF/IOA/Storage/ROOT.ML
     Author:     Olaf Mueller
 
 Memory storage case study.

--- a/src/HOL/HOLCF/IOA/Storage/Spec.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/IOA/Storage/Spec.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/IOA/example/Spec.thy
+(*  Title:      HOL/HOLCF/IOA/Storage/Spec.thy
     Author:     Olaf Müller
 *)
 

--- a/src/HOL/HOLCF/IOA/ex/ROOT.ML	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/IOA/ex/ROOT.ML	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/IOA/ex/ROOT.ML
+(*  Title:      HOL/HOLCF/IOA/ex/ROOT.ML
     Author:     Olaf Mueller
 *)
 

--- a/src/HOL/HOLCF/IOA/ex/TrivEx.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/IOA/ex/TrivEx.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/IOA/TrivEx.thy
+(*  Title:      HOL/HOLCF/IOA/ex/TrivEx.thy
     Author:     Olaf Müller
 *)
 

--- a/src/HOL/HOLCF/IOA/ex/TrivEx2.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/IOA/ex/TrivEx2.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/IOA/TrivEx.thy
+(*  Title:      HOL/HOLCF/IOA/ex/TrivEx2.thy
     Author:     Olaf Müller
 *)
 

--- a/src/HOL/HOLCF/IOA/meta_theory/Abstraction.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/IOA/meta_theory/Abstraction.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/IOA/meta_theory/Abstraction.thy
+(*  Title:      HOL/HOLCF/IOA/meta_theory/Abstraction.thy
     Author:     Olaf Müller
 *)
 

--- a/src/HOL/HOLCF/IOA/meta_theory/Asig.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/IOA/meta_theory/Asig.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/IOA/meta_theory/Asig.thy
+(*  Title:      HOL/HOLCF/IOA/meta_theory/Asig.thy
     Author:     Olaf Müller, Tobias Nipkow & Konrad Slind
 *)
 

--- a/src/HOL/HOLCF/IOA/meta_theory/Automata.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/IOA/meta_theory/Automata.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/IOA/meta_theory/Automata.thy
+(*  Title:      HOL/HOLCF/IOA/meta_theory/Automata.thy
     Author:     Olaf Müller, Konrad Slind, Tobias Nipkow
 *)
 

--- a/src/HOL/HOLCF/IOA/meta_theory/CompoExecs.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/IOA/meta_theory/CompoExecs.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/IOA/meta_theory/CompoExecs.thy
+(*  Title:      HOL/HOLCF/IOA/meta_theory/CompoExecs.thy
     Author:     Olaf Müller
 *)
 

--- a/src/HOL/HOLCF/IOA/meta_theory/CompoScheds.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/IOA/meta_theory/CompoScheds.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/IOA/meta_theory/CompoScheds.thy
+(*  Title:      HOL/HOLCF/IOA/meta_theory/CompoScheds.thy
     Author:     Olaf Müller
 *)
 

--- a/src/HOL/HOLCF/IOA/meta_theory/CompoTraces.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/IOA/meta_theory/CompoTraces.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/IOA/meta_theory/CompoTraces.thy
+(*  Title:      HOL/HOLCF/IOA/meta_theory/CompoTraces.thy
     Author:     Olaf Müller
 *) 
 

--- a/src/HOL/HOLCF/IOA/meta_theory/Compositionality.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/IOA/meta_theory/Compositionality.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/IOA/meta_theory/Compositionality.thy
+(*  Title:      HOL/HOLCF/IOA/meta_theory/Compositionality.thy
     Author:     Olaf Müller
 *)
 

--- a/src/HOL/HOLCF/IOA/meta_theory/Deadlock.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/IOA/meta_theory/Deadlock.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/IOA/meta_theory/Deadlock.thy
+(*  Title:      HOL/HOLCF/IOA/meta_theory/Deadlock.thy
     Author:     Olaf Müller
 *)
 

--- a/src/HOL/HOLCF/IOA/meta_theory/IOA.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/IOA/meta_theory/IOA.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/IOA/meta_theory/IOA.thy
+(*  Title:      HOL/HOLCF/IOA/meta_theory/IOA.thy
     Author:     Olaf Müller
 *)
 

--- a/src/HOL/HOLCF/IOA/meta_theory/LiveIOA.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/IOA/meta_theory/LiveIOA.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/IOA/meta_theory/LiveIOA.thy
+(*  Title:      HOL/HOLCF/IOA/meta_theory/LiveIOA.thy
     Author:     Olaf Müller
 *)
 

--- a/src/HOL/HOLCF/IOA/meta_theory/Pred.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/IOA/meta_theory/Pred.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/IOA/meta_theory/Pred.thy
+(*  Title:      HOL/HOLCF/IOA/meta_theory/Pred.thy
     Author:     Olaf Müller
 *)
 

--- a/src/HOL/HOLCF/IOA/meta_theory/RefCorrectness.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/IOA/meta_theory/RefCorrectness.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/IOA/meta_theory/RefCorrectness.thy
+(*  Title:      HOL/HOLCF/IOA/meta_theory/RefCorrectness.thy
     Author:     Olaf Müller
 *)
 

--- a/src/HOL/HOLCF/IOA/meta_theory/RefMappings.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/IOA/meta_theory/RefMappings.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/IOA/meta_theory/RefMappings.thy
+(*  Title:      HOL/HOLCF/IOA/meta_theory/RefMappings.thy
     Author:     Olaf Müller
 *)
 

--- a/src/HOL/HOLCF/IOA/meta_theory/Seq.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/IOA/meta_theory/Seq.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/IOA/meta_theory/Seq.thy
+(*  Title:      HOL/HOLCF/IOA/meta_theory/Seq.thy
     Author:     Olaf Müller
 *)
 

--- a/src/HOL/HOLCF/IOA/meta_theory/Sequence.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/IOA/meta_theory/Sequence.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/IOA/meta_theory/Sequence.thy
+(*  Title:      HOL/HOLCF/IOA/meta_theory/Sequence.thy
     Author:     Olaf Müller
 
 Sequences over flat domains with lifted elements.

--- a/src/HOL/HOLCF/IOA/meta_theory/ShortExecutions.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/IOA/meta_theory/ShortExecutions.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/IOA/meta_theory/ShortExecutions.thy
+(*  Title:      HOL/HOLCF/IOA/meta_theory/ShortExecutions.thy
     Author:     Olaf Müller
 *)
 

--- a/src/HOL/HOLCF/IOA/meta_theory/SimCorrectness.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/IOA/meta_theory/SimCorrectness.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/IOA/meta_theory/SimCorrectness.thy
+(*  Title:      HOL/HOLCF/IOA/meta_theory/SimCorrectness.thy
     Author:     Olaf Müller
 *)
 

--- a/src/HOL/HOLCF/IOA/meta_theory/Simulations.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/IOA/meta_theory/Simulations.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/IOA/meta_theory/Simulations.thy
+(*  Title:      HOL/HOLCF/IOA/meta_theory/Simulations.thy
     Author:     Olaf Müller
 *)
 

--- a/src/HOL/HOLCF/IOA/meta_theory/TL.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/IOA/meta_theory/TL.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/IOA/meta_theory/TLS.thy
+(*  Title:      HOL/HOLCF/IOA/meta_theory/TL.thy
     Author:     Olaf Müller
 *)
 

--- a/src/HOL/HOLCF/IOA/meta_theory/TLS.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/IOA/meta_theory/TLS.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/IOA/meta_theory/TLS.thy
+(*  Title:      HOL/HOLCF/IOA/meta_theory/TLS.thy
     Author:     Olaf Müller
 *)
 

--- a/src/HOL/HOLCF/IOA/meta_theory/Traces.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/IOA/meta_theory/Traces.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/IOA/meta_theory/Traces.thy
+(*  Title:      HOL/HOLCF/IOA/meta_theory/Traces.thy
     Author:     Olaf Müller
 *)
 

--- a/src/HOL/HOLCF/Library/Bool_Discrete.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/Library/Bool_Discrete.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/Library/Bool_Discrete.thy
+(*  Title:      HOL/HOLCF/Library/Bool_Discrete.thy
     Author:     Brian Huffman
 *)
 

--- a/src/HOL/HOLCF/Library/Char_Discrete.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/Library/Char_Discrete.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/Library/Char_Discrete.thy
+(*  Title:      HOL/HOLCF/Library/Char_Discrete.thy
     Author:     Brian Huffman
 *)
 

--- a/src/HOL/HOLCF/Library/Defl_Bifinite.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/Library/Defl_Bifinite.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/Library/Defl_Bifinite.thy
+(*  Title:      HOL/HOLCF/Library/Defl_Bifinite.thy
     Author:     Brian Huffman
 *)
 

--- a/src/HOL/HOLCF/Library/HOL_Cpo.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/Library/HOL_Cpo.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/HOL_Cpo.thy
+(*  Title:      HOL/HOLCF/Library/HOL_Cpo.thy
     Author:     Brian Huffman
 *)
 

--- a/src/HOL/HOLCF/Library/Int_Discrete.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/Library/Int_Discrete.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/Library/Int_Discrete.thy
+(*  Title:      HOL/HOLCF/Library/Int_Discrete.thy
     Author:     Brian Huffman
 *)
 

--- a/src/HOL/HOLCF/Library/List_Cpo.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/Library/List_Cpo.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/Library/List_Cpo.thy
+(*  Title:      HOL/HOLCF/Library/List_Cpo.thy
     Author:     Brian Huffman
 *)
 

--- a/src/HOL/HOLCF/Library/List_Predomain.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/Library/List_Predomain.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/Library/List_Predomain.thy
+(*  Title:      HOL/HOLCF/Library/List_Predomain.thy
     Author:     Brian Huffman
 *)
 

--- a/src/HOL/HOLCF/Library/Nat_Discrete.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/Library/Nat_Discrete.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/Library/Nat_Discrete.thy
+(*  Title:      HOL/HOLCF/Library/Nat_Discrete.thy
     Author:     Brian Huffman
 *)
 

--- a/src/HOL/HOLCF/Library/Option_Cpo.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/Library/Option_Cpo.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/Option_Cpo.thy
+(*  Title:      HOL/HOLCF/Library/Option_Cpo.thy
     Author:     Brian Huffman
 *)
 

--- a/src/HOL/HOLCF/Library/Stream.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/Library/Stream.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/ex/Stream.thy
+(*  Title:      HOL/HOLCF/Library/Stream.thy
     Author:     Franz Regensburger, David von Oheimb, Borislav Gajanovic
 *)
 

--- a/src/HOL/HOLCF/Library/Sum_Cpo.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/Library/Sum_Cpo.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/Sum_Cpo.thy
+(*  Title:      HOL/HOLCF/Library/Sum_Cpo.thy
     Author:     Brian Huffman
 *)
 

--- a/src/HOL/HOLCF/Lift.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/Lift.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/Lift.thy
+(*  Title:      HOL/HOLCF/Lift.thy
     Author:     Olaf Mueller
 *)
 

--- a/src/HOL/HOLCF/LowerPD.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/LowerPD.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/LowerPD.thy
+(*  Title:      HOL/HOLCF/LowerPD.thy
     Author:     Brian Huffman
 *)
 

--- a/src/HOL/HOLCF/Map_Functions.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/Map_Functions.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/Map_Functions.thy
+(*  Title:      HOL/HOLCF/Map_Functions.thy
     Author:     Brian Huffman
 *)
 

--- a/src/HOL/HOLCF/One.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/One.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/One.thy
+(*  Title:      HOL/HOLCF/One.thy
     Author:     Oscar Slotosch
 *)
 

--- a/src/HOL/HOLCF/Pcpo.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/Pcpo.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/Pcpo.thy
+(*  Title:      HOL/HOLCF/Pcpo.thy
     Author:     Franz Regensburger
 *)
 

--- a/src/HOL/HOLCF/Plain_HOLCF.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/Plain_HOLCF.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/Plain_HOLCF.thy
+(*  Title:      HOL/HOLCF/Plain_HOLCF.thy
     Author:     Brian Huffman
 *)
 

--- a/src/HOL/HOLCF/Porder.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/Porder.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/Porder.thy
+(*  Title:      HOL/HOLCF/Porder.thy
     Author:     Franz Regensburger and Brian Huffman
 *)
 

--- a/src/HOL/HOLCF/Powerdomains.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/Powerdomains.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/Powerdomains.thy
+(*  Title:      HOL/HOLCF/Powerdomains.thy
     Author:     Brian Huffman
 *)
 

--- a/src/HOL/HOLCF/Product_Cpo.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/Product_Cpo.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/Product_Cpo.thy
+(*  Title:      HOL/HOLCF/Product_Cpo.thy
     Author:     Franz Regensburger
 *)
 

--- a/src/HOL/HOLCF/ROOT.ML	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/ROOT.ML	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/ROOT.ML
+(*  Title:      HOL/HOLCF/ROOT.ML
     Author:     Franz Regensburger
 
 HOLCF -- a semantic extension of HOL by the LCF logic.

--- a/src/HOL/HOLCF/Representable.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/Representable.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/Representable.thy
+(*  Title:      HOL/HOLCF/Representable.thy
     Author:     Brian Huffman
 *)
 

--- a/src/HOL/HOLCF/Sfun.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/Sfun.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/Sfun.thy
+(*  Title:      HOL/HOLCF/Sfun.thy
     Author:     Brian Huffman
 *)
 

--- a/src/HOL/HOLCF/Sprod.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/Sprod.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/Sprod.thy
+(*  Title:      HOL/HOLCF/Sprod.thy
     Author:     Franz Regensburger
     Author:     Brian Huffman
 *)

--- a/src/HOL/HOLCF/Ssum.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/Ssum.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/Ssum.thy
+(*  Title:      HOL/HOLCF/Ssum.thy
     Author:     Franz Regensburger
     Author:     Brian Huffman
 *)

--- a/src/HOL/HOLCF/Tools/Domain/domain.ML	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/Tools/Domain/domain.ML	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/Tools/Domain/domain.ML
+(*  Title:      HOL/HOLCF/Tools/Domain/domain.ML
     Author:     David von Oheimb
     Author:     Brian Huffman
 

--- a/src/HOL/HOLCF/Tools/Domain/domain_axioms.ML	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/Tools/Domain/domain_axioms.ML	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/Tools/Domain/domain_axioms.ML
+(*  Title:      HOL/HOLCF/Tools/Domain/domain_axioms.ML
     Author:     David von Oheimb
     Author:     Brian Huffman
 

--- a/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/Tools/Domain/domain_constructors.ML
+(*  Title:      HOL/HOLCF/Tools/Domain/domain_constructors.ML
     Author:     Brian Huffman
 
 Defines constructor functions for a given domain isomorphism

--- a/src/HOL/HOLCF/Tools/Domain/domain_induction.ML	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/Tools/Domain/domain_induction.ML	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/Tools/Domain/domain_induction.ML
+(*  Title:      HOL/HOLCF/Tools/Domain/domain_induction.ML
     Author:     David von Oheimb
     Author:     Brian Huffman
 

--- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/Tools/Domain/domain_isomorphism.ML
+(*  Title:      HOL/HOLCF/Tools/Domain/domain_isomorphism.ML
     Author:     Brian Huffman
 
 Defines new types satisfying the given domain equations.

--- a/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/Tools/Domain/domain_take_proofs.ML
+(*  Title:      HOL/HOLCF/Tools/Domain/domain_take_proofs.ML
     Author:     Brian Huffman
 
 Defines take functions for the given domain equation

--- a/src/HOL/HOLCF/Tools/cont_consts.ML	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/Tools/cont_consts.ML	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/Tools/cont_consts.ML
+(*  Title:      HOL/HOLCF/Tools/cont_consts.ML
     Author:     Tobias Mayr, David von Oheimb, and Markus Wenzel
 
 HOLCF version of consts: handle continuous function types in mixfix

--- a/src/HOL/HOLCF/Tools/cont_proc.ML	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/Tools/cont_proc.ML	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/Tools/cont_proc.ML
+(*  Title:      HOL/HOLCF/Tools/cont_proc.ML
     Author:     Brian Huffman
 *)
 

--- a/src/HOL/HOLCF/Tools/cpodef.ML	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/Tools/cpodef.ML	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/Tools/cpodef.ML
+(*  Title:      HOL/HOLCF/Tools/cpodef.ML
     Author:     Brian Huffman
 
 Primitive domain definitions for HOLCF, similar to Gordon/HOL-style

--- a/src/HOL/HOLCF/Tools/domaindef.ML	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/Tools/domaindef.ML	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/Tools/repdef.ML
+(*  Title:      HOL/HOLCF/Tools/domaindef.ML
     Author:     Brian Huffman
 
 Defining representable domains using algebraic deflations.

--- a/src/HOL/HOLCF/Tools/fixrec.ML	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/Tools/fixrec.ML	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/Tools/fixrec.ML
+(*  Title:      HOL/HOLCF/Tools/fixrec.ML
     Author:     Amber Telfer and Brian Huffman
 
 Recursive function definition package for HOLCF.

--- a/src/HOL/HOLCF/Tools/holcf_library.ML	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/Tools/holcf_library.ML	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/Tools/holcf_library.ML
+(*  Title:      HOL/HOLCF/Tools/holcf_library.ML
     Author:     Brian Huffman
 
 Functions for constructing HOLCF types and terms.

--- a/src/HOL/HOLCF/Tr.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/Tr.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/Tr.thy
+(*  Title:      HOL/HOLCF/Tr.thy
     Author:     Franz Regensburger
 *)
 

--- a/src/HOL/HOLCF/Tutorial/Domain_ex.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/Tutorial/Domain_ex.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/ex/Domain_ex.thy
+(*  Title:      HOL/HOLCF/Tutorial/Domain_ex.thy
     Author:     Brian Huffman
 *)
 

--- a/src/HOL/HOLCF/Tutorial/Fixrec_ex.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/Tutorial/Fixrec_ex.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/ex/Fixrec_ex.thy
+(*  Title:      HOL/HOLCF/Tutorial/Fixrec_ex.thy
     Author:     Brian Huffman
 *)
 

--- a/src/HOL/HOLCF/Tutorial/New_Domain.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/Tutorial/New_Domain.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/ex/New_Domain.thy
+(*  Title:      HOL/HOLCF/Tutorial/New_Domain.thy
     Author:     Brian Huffman
 *)
 

--- a/src/HOL/HOLCF/Universal.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/Universal.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/Universal.thy
+(*  Title:      HOL/HOLCF/Universal.thy
     Author:     Brian Huffman
 *)
 

--- a/src/HOL/HOLCF/Up.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/Up.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/Up.thy
+(*  Title:      HOL/HOLCF/Up.thy
     Author:     Franz Regensburger
     Author:     Brian Huffman
 *)

--- a/src/HOL/HOLCF/UpperPD.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/UpperPD.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/UpperPD.thy
+(*  Title:      HOL/HOLCF/UpperPD.thy
     Author:     Brian Huffman
 *)
 

--- a/src/HOL/HOLCF/ex/Dnat.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/ex/Dnat.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/Dnat.thy
+(*  Title:      HOL/HOLCF/ex/Dnat.thy
     Author:     Franz Regensburger
 
 Theory for the domain of natural numbers  dnat = one ++ dnat

--- a/src/HOL/HOLCF/ex/Domain_Proofs.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/ex/Domain_Proofs.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/ex/Domain_Proofs.thy
+(*  Title:      HOL/HOLCF/ex/Domain_Proofs.thy
     Author:     Brian Huffman
 *)
 

--- a/src/HOL/HOLCF/ex/Fix2.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/ex/Fix2.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/ex/Fix2.thy
+(*  Title:      HOL/HOLCF/ex/Fix2.thy
     Author:     Franz Regensburger
 
 Show that fix is the unique least fixed-point operator.

--- a/src/HOL/HOLCF/ex/Hoare.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/ex/Hoare.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/ex/hoare.thy
+(*  Title:      HOL/HOLCF/ex/Hoare.thy
     Author:     Franz Regensburger
 
 Theory for an example by C.A.R. Hoare

--- a/src/HOL/HOLCF/ex/Letrec.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/ex/Letrec.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/ex/Letrec.thy
+(*  Title:      HOL/HOLCF/ex/Letrec.thy
     Author:     Brian Huffman
 *)
 

--- a/src/HOL/HOLCF/ex/Loop.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/ex/Loop.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/ex/Loop.thy
+(*  Title:      HOL/HOLCF/ex/Loop.thy
     Author:     Franz Regensburger
 *)
 

--- a/src/HOL/HOLCF/ex/Pattern_Match.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/ex/Pattern_Match.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/ex/Pattern_Match.thy
+(*  Title:      HOL/HOLCF/ex/Pattern_Match.thy
     Author:     Brian Huffman
 *)
 

--- a/src/HOL/HOLCF/ex/Powerdomain_ex.thy	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/ex/Powerdomain_ex.thy	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/ex/Powerdomain_ex.thy
+(*  Title:      HOL/HOLCF/ex/Powerdomain_ex.thy
     Author:     Brian Huffman
 *)
 

--- a/src/HOL/HOLCF/ex/ROOT.ML	Tue Mar 29 17:30:26 2011 +0200
+++ b/src/HOL/HOLCF/ex/ROOT.ML	Tue Mar 29 17:47:11 2011 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/ex/ROOT.ML
+(*  Title:      HOL/HOLCF/ex/ROOT.ML
 
 Misc HOLCF examples.
 *)