tuned headers;
authorwenzelm
Tue Mar 29 17:47:11 2011 +0200 (2011-03-29)
changeset 421514da4fc77664b
parent 42150 b0c0638c4aad
child 42152 6c17259724b2
child 42157 99e359a9db27
tuned headers;
src/HOL/HOLCF/Bifinite.thy
src/HOL/HOLCF/Cfun.thy
src/HOL/HOLCF/Compact_Basis.thy
src/HOL/HOLCF/Completion.thy
src/HOL/HOLCF/Cont.thy
src/HOL/HOLCF/ConvexPD.thy
src/HOL/HOLCF/Cpodef.thy
src/HOL/HOLCF/Cprod.thy
src/HOL/HOLCF/Deflation.thy
src/HOL/HOLCF/Discrete.thy
src/HOL/HOLCF/Domain.thy
src/HOL/HOLCF/Domain_Aux.thy
src/HOL/HOLCF/FOCUS/Buffer.thy
src/HOL/HOLCF/FOCUS/Buffer_adm.thy
src/HOL/HOLCF/FOCUS/FOCUS.thy
src/HOL/HOLCF/FOCUS/Fstream.thy
src/HOL/HOLCF/FOCUS/Fstreams.thy
src/HOL/HOLCF/FOCUS/Stream_adm.thy
src/HOL/HOLCF/Fix.thy
src/HOL/HOLCF/Fixrec.thy
src/HOL/HOLCF/Fun_Cpo.thy
src/HOL/HOLCF/HOLCF.thy
src/HOL/HOLCF/IMP/Denotational.thy
src/HOL/HOLCF/IMP/HoareEx.thy
src/HOL/HOLCF/IOA/ABP/Abschannel.thy
src/HOL/HOLCF/IOA/ABP/Abschannel_finite.thy
src/HOL/HOLCF/IOA/ABP/Action.thy
src/HOL/HOLCF/IOA/ABP/Check.ML
src/HOL/HOLCF/IOA/ABP/Correctness.thy
src/HOL/HOLCF/IOA/ABP/Env.thy
src/HOL/HOLCF/IOA/ABP/Impl.thy
src/HOL/HOLCF/IOA/ABP/Impl_finite.thy
src/HOL/HOLCF/IOA/ABP/Lemmas.thy
src/HOL/HOLCF/IOA/ABP/Packet.thy
src/HOL/HOLCF/IOA/ABP/ROOT.ML
src/HOL/HOLCF/IOA/ABP/Receiver.thy
src/HOL/HOLCF/IOA/ABP/Sender.thy
src/HOL/HOLCF/IOA/ABP/Spec.thy
src/HOL/HOLCF/IOA/NTP/Abschannel.thy
src/HOL/HOLCF/IOA/NTP/Action.thy
src/HOL/HOLCF/IOA/NTP/Correctness.thy
src/HOL/HOLCF/IOA/NTP/Impl.thy
src/HOL/HOLCF/IOA/NTP/Lemmas.thy
src/HOL/HOLCF/IOA/NTP/Multiset.thy
src/HOL/HOLCF/IOA/NTP/Packet.thy
src/HOL/HOLCF/IOA/NTP/ROOT.ML
src/HOL/HOLCF/IOA/NTP/Receiver.thy
src/HOL/HOLCF/IOA/NTP/Sender.thy
src/HOL/HOLCF/IOA/NTP/Spec.thy
src/HOL/HOLCF/IOA/ROOT.ML
src/HOL/HOLCF/IOA/Storage/Action.thy
src/HOL/HOLCF/IOA/Storage/Correctness.thy
src/HOL/HOLCF/IOA/Storage/Impl.thy
src/HOL/HOLCF/IOA/Storage/ROOT.ML
src/HOL/HOLCF/IOA/Storage/Spec.thy
src/HOL/HOLCF/IOA/ex/ROOT.ML
src/HOL/HOLCF/IOA/ex/TrivEx.thy
src/HOL/HOLCF/IOA/ex/TrivEx2.thy
src/HOL/HOLCF/IOA/meta_theory/Abstraction.thy
src/HOL/HOLCF/IOA/meta_theory/Asig.thy
src/HOL/HOLCF/IOA/meta_theory/Automata.thy
src/HOL/HOLCF/IOA/meta_theory/CompoExecs.thy
src/HOL/HOLCF/IOA/meta_theory/CompoScheds.thy
src/HOL/HOLCF/IOA/meta_theory/CompoTraces.thy
src/HOL/HOLCF/IOA/meta_theory/Compositionality.thy
src/HOL/HOLCF/IOA/meta_theory/Deadlock.thy
src/HOL/HOLCF/IOA/meta_theory/IOA.thy
src/HOL/HOLCF/IOA/meta_theory/LiveIOA.thy
src/HOL/HOLCF/IOA/meta_theory/Pred.thy
src/HOL/HOLCF/IOA/meta_theory/RefCorrectness.thy
src/HOL/HOLCF/IOA/meta_theory/RefMappings.thy
src/HOL/HOLCF/IOA/meta_theory/Seq.thy
src/HOL/HOLCF/IOA/meta_theory/Sequence.thy
src/HOL/HOLCF/IOA/meta_theory/ShortExecutions.thy
src/HOL/HOLCF/IOA/meta_theory/SimCorrectness.thy
src/HOL/HOLCF/IOA/meta_theory/Simulations.thy
src/HOL/HOLCF/IOA/meta_theory/TL.thy
src/HOL/HOLCF/IOA/meta_theory/TLS.thy
src/HOL/HOLCF/IOA/meta_theory/Traces.thy
src/HOL/HOLCF/Library/Bool_Discrete.thy
src/HOL/HOLCF/Library/Char_Discrete.thy
src/HOL/HOLCF/Library/Defl_Bifinite.thy
src/HOL/HOLCF/Library/HOL_Cpo.thy
src/HOL/HOLCF/Library/Int_Discrete.thy
src/HOL/HOLCF/Library/List_Cpo.thy
src/HOL/HOLCF/Library/List_Predomain.thy
src/HOL/HOLCF/Library/Nat_Discrete.thy
src/HOL/HOLCF/Library/Option_Cpo.thy
src/HOL/HOLCF/Library/Stream.thy
src/HOL/HOLCF/Library/Sum_Cpo.thy
src/HOL/HOLCF/Lift.thy
src/HOL/HOLCF/LowerPD.thy
src/HOL/HOLCF/Map_Functions.thy
src/HOL/HOLCF/One.thy
src/HOL/HOLCF/Pcpo.thy
src/HOL/HOLCF/Plain_HOLCF.thy
src/HOL/HOLCF/Porder.thy
src/HOL/HOLCF/Powerdomains.thy
src/HOL/HOLCF/Product_Cpo.thy
src/HOL/HOLCF/ROOT.ML
src/HOL/HOLCF/Representable.thy
src/HOL/HOLCF/Sfun.thy
src/HOL/HOLCF/Sprod.thy
src/HOL/HOLCF/Ssum.thy
src/HOL/HOLCF/Tools/Domain/domain.ML
src/HOL/HOLCF/Tools/Domain/domain_axioms.ML
src/HOL/HOLCF/Tools/Domain/domain_constructors.ML
src/HOL/HOLCF/Tools/Domain/domain_induction.ML
src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML
src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML
src/HOL/HOLCF/Tools/cont_consts.ML
src/HOL/HOLCF/Tools/cont_proc.ML
src/HOL/HOLCF/Tools/cpodef.ML
src/HOL/HOLCF/Tools/domaindef.ML
src/HOL/HOLCF/Tools/fixrec.ML
src/HOL/HOLCF/Tools/holcf_library.ML
src/HOL/HOLCF/Tr.thy
src/HOL/HOLCF/Tutorial/Domain_ex.thy
src/HOL/HOLCF/Tutorial/Fixrec_ex.thy
src/HOL/HOLCF/Tutorial/New_Domain.thy
src/HOL/HOLCF/Universal.thy
src/HOL/HOLCF/Up.thy
src/HOL/HOLCF/UpperPD.thy
src/HOL/HOLCF/ex/Dnat.thy
src/HOL/HOLCF/ex/Domain_Proofs.thy
src/HOL/HOLCF/ex/Fix2.thy
src/HOL/HOLCF/ex/Hoare.thy
src/HOL/HOLCF/ex/Letrec.thy
src/HOL/HOLCF/ex/Loop.thy
src/HOL/HOLCF/ex/Pattern_Match.thy
src/HOL/HOLCF/ex/Powerdomain_ex.thy
src/HOL/HOLCF/ex/ROOT.ML
     1.1 --- a/src/HOL/HOLCF/Bifinite.thy	Tue Mar 29 17:30:26 2011 +0200
     1.2 +++ b/src/HOL/HOLCF/Bifinite.thy	Tue Mar 29 17:47:11 2011 +0200
     1.3 @@ -1,4 +1,4 @@
     1.4 -(*  Title:      HOLCF/Bifinite.thy
     1.5 +(*  Title:      HOL/HOLCF/Bifinite.thy
     1.6      Author:     Brian Huffman
     1.7  *)
     1.8  
     2.1 --- a/src/HOL/HOLCF/Cfun.thy	Tue Mar 29 17:30:26 2011 +0200
     2.2 +++ b/src/HOL/HOLCF/Cfun.thy	Tue Mar 29 17:47:11 2011 +0200
     2.3 @@ -1,4 +1,4 @@
     2.4 -(*  Title:      HOLCF/Cfun.thy
     2.5 +(*  Title:      HOL/HOLCF/Cfun.thy
     2.6      Author:     Franz Regensburger
     2.7      Author:     Brian Huffman
     2.8  *)
     3.1 --- a/src/HOL/HOLCF/Compact_Basis.thy	Tue Mar 29 17:30:26 2011 +0200
     3.2 +++ b/src/HOL/HOLCF/Compact_Basis.thy	Tue Mar 29 17:47:11 2011 +0200
     3.3 @@ -1,4 +1,4 @@
     3.4 -(*  Title:      HOLCF/Compact_Basis.thy
     3.5 +(*  Title:      HOL/HOLCF/Compact_Basis.thy
     3.6      Author:     Brian Huffman
     3.7  *)
     3.8  
     4.1 --- a/src/HOL/HOLCF/Completion.thy	Tue Mar 29 17:30:26 2011 +0200
     4.2 +++ b/src/HOL/HOLCF/Completion.thy	Tue Mar 29 17:47:11 2011 +0200
     4.3 @@ -1,4 +1,4 @@
     4.4 -(*  Title:      HOLCF/Completion.thy
     4.5 +(*  Title:      HOL/HOLCF/Completion.thy
     4.6      Author:     Brian Huffman
     4.7  *)
     4.8  
     5.1 --- a/src/HOL/HOLCF/Cont.thy	Tue Mar 29 17:30:26 2011 +0200
     5.2 +++ b/src/HOL/HOLCF/Cont.thy	Tue Mar 29 17:47:11 2011 +0200
     5.3 @@ -1,4 +1,4 @@
     5.4 -(*  Title:      HOLCF/Cont.thy
     5.5 +(*  Title:      HOL/HOLCF/Cont.thy
     5.6      Author:     Franz Regensburger
     5.7      Author:     Brian Huffman
     5.8  *)
     6.1 --- a/src/HOL/HOLCF/ConvexPD.thy	Tue Mar 29 17:30:26 2011 +0200
     6.2 +++ b/src/HOL/HOLCF/ConvexPD.thy	Tue Mar 29 17:47:11 2011 +0200
     6.3 @@ -1,4 +1,4 @@
     6.4 -(*  Title:      HOLCF/ConvexPD.thy
     6.5 +(*  Title:      HOL/HOLCF/ConvexPD.thy
     6.6      Author:     Brian Huffman
     6.7  *)
     6.8  
     7.1 --- a/src/HOL/HOLCF/Cpodef.thy	Tue Mar 29 17:30:26 2011 +0200
     7.2 +++ b/src/HOL/HOLCF/Cpodef.thy	Tue Mar 29 17:47:11 2011 +0200
     7.3 @@ -1,4 +1,4 @@
     7.4 -(*  Title:      HOLCF/Pcpodef.thy
     7.5 +(*  Title:      HOL/HOLCF/Cpodef.thy
     7.6      Author:     Brian Huffman
     7.7  *)
     7.8  
     8.1 --- a/src/HOL/HOLCF/Cprod.thy	Tue Mar 29 17:30:26 2011 +0200
     8.2 +++ b/src/HOL/HOLCF/Cprod.thy	Tue Mar 29 17:47:11 2011 +0200
     8.3 @@ -1,4 +1,4 @@
     8.4 -(*  Title:      HOLCF/Cprod.thy
     8.5 +(*  Title:      HOL/HOLCF/Cprod.thy
     8.6      Author:     Franz Regensburger
     8.7  *)
     8.8  
     9.1 --- a/src/HOL/HOLCF/Deflation.thy	Tue Mar 29 17:30:26 2011 +0200
     9.2 +++ b/src/HOL/HOLCF/Deflation.thy	Tue Mar 29 17:47:11 2011 +0200
     9.3 @@ -1,4 +1,4 @@
     9.4 -(*  Title:      HOLCF/Deflation.thy
     9.5 +(*  Title:      HOL/HOLCF/Deflation.thy
     9.6      Author:     Brian Huffman
     9.7  *)
     9.8  
    10.1 --- a/src/HOL/HOLCF/Discrete.thy	Tue Mar 29 17:30:26 2011 +0200
    10.2 +++ b/src/HOL/HOLCF/Discrete.thy	Tue Mar 29 17:47:11 2011 +0200
    10.3 @@ -1,4 +1,4 @@
    10.4 -(*  Title:      HOLCF/Discrete.thy
    10.5 +(*  Title:      HOL/HOLCF/Discrete.thy
    10.6      Author:     Tobias Nipkow
    10.7  *)
    10.8  
    11.1 --- a/src/HOL/HOLCF/Domain.thy	Tue Mar 29 17:30:26 2011 +0200
    11.2 +++ b/src/HOL/HOLCF/Domain.thy	Tue Mar 29 17:47:11 2011 +0200
    11.3 @@ -1,4 +1,4 @@
    11.4 -(*  Title:      HOLCF/Domain.thy
    11.5 +(*  Title:      HOL/HOLCF/Domain.thy
    11.6      Author:     Brian Huffman
    11.7  *)
    11.8  
    12.1 --- a/src/HOL/HOLCF/Domain_Aux.thy	Tue Mar 29 17:30:26 2011 +0200
    12.2 +++ b/src/HOL/HOLCF/Domain_Aux.thy	Tue Mar 29 17:47:11 2011 +0200
    12.3 @@ -1,4 +1,4 @@
    12.4 -(*  Title:      HOLCF/Domain_Aux.thy
    12.5 +(*  Title:      HOL/HOLCF/Domain_Aux.thy
    12.6      Author:     Brian Huffman
    12.7  *)
    12.8  
    13.1 --- a/src/HOL/HOLCF/FOCUS/Buffer.thy	Tue Mar 29 17:30:26 2011 +0200
    13.2 +++ b/src/HOL/HOLCF/FOCUS/Buffer.thy	Tue Mar 29 17:47:11 2011 +0200
    13.3 @@ -1,4 +1,4 @@
    13.4 -(*  Title:      HOLCF/FOCUS/Buffer.thy
    13.5 +(*  Title:      HOL/HOLCF/FOCUS/Buffer.thy
    13.6      Author:     David von Oheimb, TU Muenchen
    13.7  
    13.8  Formalization of section 4 of
    14.1 --- a/src/HOL/HOLCF/FOCUS/Buffer_adm.thy	Tue Mar 29 17:30:26 2011 +0200
    14.2 +++ b/src/HOL/HOLCF/FOCUS/Buffer_adm.thy	Tue Mar 29 17:47:11 2011 +0200
    14.3 @@ -1,4 +1,4 @@
    14.4 -(*  Title:      HOLCF/FOCUS/Buffer_adm.thy
    14.5 +(*  Title:      HOL/HOLCF/FOCUS/Buffer_adm.thy
    14.6      Author:     David von Oheimb, TU Muenchen
    14.7  *)
    14.8  
    15.1 --- a/src/HOL/HOLCF/FOCUS/FOCUS.thy	Tue Mar 29 17:30:26 2011 +0200
    15.2 +++ b/src/HOL/HOLCF/FOCUS/FOCUS.thy	Tue Mar 29 17:47:11 2011 +0200
    15.3 @@ -1,4 +1,4 @@
    15.4 -(*  Title:      HOLCF/FOCUS/FOCUS.thy
    15.5 +(*  Title:      HOL/HOLCF/FOCUS/FOCUS.thy
    15.6      Author:     David von Oheimb, TU Muenchen
    15.7  *)
    15.8  
    16.1 --- a/src/HOL/HOLCF/FOCUS/Fstream.thy	Tue Mar 29 17:30:26 2011 +0200
    16.2 +++ b/src/HOL/HOLCF/FOCUS/Fstream.thy	Tue Mar 29 17:47:11 2011 +0200
    16.3 @@ -1,4 +1,4 @@
    16.4 -(*  Title:      HOLCF/FOCUS/Fstream.thy
    16.5 +(*  Title:      HOL/HOLCF/FOCUS/Fstream.thy
    16.6      Author:     David von Oheimb, TU Muenchen
    16.7  
    16.8  FOCUS streams (with lifted elements).
    17.1 --- a/src/HOL/HOLCF/FOCUS/Fstreams.thy	Tue Mar 29 17:30:26 2011 +0200
    17.2 +++ b/src/HOL/HOLCF/FOCUS/Fstreams.thy	Tue Mar 29 17:47:11 2011 +0200
    17.3 @@ -1,4 +1,4 @@
    17.4 -(*  Title:      HOLCF/FOCUS/Fstreams.thy
    17.5 +(*  Title:      HOL/HOLCF/FOCUS/Fstreams.thy
    17.6      Author:     Borislav Gajanovic
    17.7  
    17.8  FOCUS flat streams (with lifted elements).
    18.1 --- a/src/HOL/HOLCF/FOCUS/Stream_adm.thy	Tue Mar 29 17:30:26 2011 +0200
    18.2 +++ b/src/HOL/HOLCF/FOCUS/Stream_adm.thy	Tue Mar 29 17:47:11 2011 +0200
    18.3 @@ -1,4 +1,4 @@
    18.4 -(*  Title:      HOLCF/ex/Stream_adm.thy
    18.5 +(*  Title:      HOL/HOLCF/FOCUS/Stream_adm.thy
    18.6      Author:     David von Oheimb, TU Muenchen
    18.7  *)
    18.8  
    19.1 --- a/src/HOL/HOLCF/Fix.thy	Tue Mar 29 17:30:26 2011 +0200
    19.2 +++ b/src/HOL/HOLCF/Fix.thy	Tue Mar 29 17:47:11 2011 +0200
    19.3 @@ -1,4 +1,4 @@
    19.4 -(*  Title:      HOLCF/Fix.thy
    19.5 +(*  Title:      HOL/HOLCF/Fix.thy
    19.6      Author:     Franz Regensburger
    19.7      Author:     Brian Huffman
    19.8  *)
    20.1 --- a/src/HOL/HOLCF/Fixrec.thy	Tue Mar 29 17:30:26 2011 +0200
    20.2 +++ b/src/HOL/HOLCF/Fixrec.thy	Tue Mar 29 17:47:11 2011 +0200
    20.3 @@ -1,4 +1,4 @@
    20.4 -(*  Title:      HOLCF/Fixrec.thy
    20.5 +(*  Title:      HOL/HOLCF/Fixrec.thy
    20.6      Author:     Amber Telfer and Brian Huffman
    20.7  *)
    20.8  
    21.1 --- a/src/HOL/HOLCF/Fun_Cpo.thy	Tue Mar 29 17:30:26 2011 +0200
    21.2 +++ b/src/HOL/HOLCF/Fun_Cpo.thy	Tue Mar 29 17:47:11 2011 +0200
    21.3 @@ -1,4 +1,4 @@
    21.4 -(*  Title:      HOLCF/Fun_Cpo.thy
    21.5 +(*  Title:      HOL/HOLCF/Fun_Cpo.thy
    21.6      Author:     Franz Regensburger
    21.7      Author:     Brian Huffman
    21.8  *)
    22.1 --- a/src/HOL/HOLCF/HOLCF.thy	Tue Mar 29 17:30:26 2011 +0200
    22.2 +++ b/src/HOL/HOLCF/HOLCF.thy	Tue Mar 29 17:47:11 2011 +0200
    22.3 @@ -1,4 +1,4 @@
    22.4 -(*  Title:      HOLCF/HOLCF.thy
    22.5 +(*  Title:      HOL/HOLCF/HOLCF.thy
    22.6      Author:     Franz Regensburger
    22.7  
    22.8  HOLCF -- a semantic extension of HOL by the LCF logic.
    23.1 --- a/src/HOL/HOLCF/IMP/Denotational.thy	Tue Mar 29 17:30:26 2011 +0200
    23.2 +++ b/src/HOL/HOLCF/IMP/Denotational.thy	Tue Mar 29 17:47:11 2011 +0200
    23.3 @@ -1,4 +1,4 @@
    23.4 -(*  Title:      HOLCF/IMP/Denotational.thy
    23.5 +(*  Title:      HOL/HOLCF/IMP/Denotational.thy
    23.6      Author:     Tobias Nipkow and Robert Sandner, TUM
    23.7      Copyright   1996 TUM
    23.8  *)
    24.1 --- a/src/HOL/HOLCF/IMP/HoareEx.thy	Tue Mar 29 17:30:26 2011 +0200
    24.2 +++ b/src/HOL/HOLCF/IMP/HoareEx.thy	Tue Mar 29 17:47:11 2011 +0200
    24.3 @@ -1,4 +1,4 @@
    24.4 -(*  Title:      HOLCF/IMP/HoareEx.thy
    24.5 +(*  Title:      HOL/HOLCF/IMP/HoareEx.thy
    24.6      Author:     Tobias Nipkow, TUM
    24.7      Copyright   1997 TUM
    24.8  *)
    25.1 --- a/src/HOL/HOLCF/IOA/ABP/Abschannel.thy	Tue Mar 29 17:30:26 2011 +0200
    25.2 +++ b/src/HOL/HOLCF/IOA/ABP/Abschannel.thy	Tue Mar 29 17:47:11 2011 +0200
    25.3 @@ -1,4 +1,4 @@
    25.4 -(*  Title:      HOLCF/IOA/ABP/Abschannel.thy
    25.5 +(*  Title:      HOL/HOLCF/IOA/ABP/Abschannel.thy
    25.6      Author:     Olaf Müller
    25.7  *)
    25.8  
    26.1 --- a/src/HOL/HOLCF/IOA/ABP/Abschannel_finite.thy	Tue Mar 29 17:30:26 2011 +0200
    26.2 +++ b/src/HOL/HOLCF/IOA/ABP/Abschannel_finite.thy	Tue Mar 29 17:47:11 2011 +0200
    26.3 @@ -1,4 +1,4 @@
    26.4 -(*  Title:      HOLCF/IOA/ABP/Abschannels.thy
    26.5 +(*  Title:      HOL/HOLCF/IOA/ABP/Abschannel_finite.thy
    26.6      Author:     Olaf Müller
    26.7  *)
    26.8  
    27.1 --- a/src/HOL/HOLCF/IOA/ABP/Action.thy	Tue Mar 29 17:30:26 2011 +0200
    27.2 +++ b/src/HOL/HOLCF/IOA/ABP/Action.thy	Tue Mar 29 17:47:11 2011 +0200
    27.3 @@ -1,4 +1,4 @@
    27.4 -(*  Title:      HOLCF/IOA/ABP/Action.thy
    27.5 +(*  Title:      HOL/HOLCF/IOA/ABP/Action.thy
    27.6      Author:     Olaf Müller
    27.7  *)
    27.8  
    28.1 --- a/src/HOL/HOLCF/IOA/ABP/Check.ML	Tue Mar 29 17:30:26 2011 +0200
    28.2 +++ b/src/HOL/HOLCF/IOA/ABP/Check.ML	Tue Mar 29 17:47:11 2011 +0200
    28.3 @@ -1,4 +1,4 @@
    28.4 -(*  Title:      HOLCF/IOA/ABP/Check.ML
    28.5 +(*  Title:      HOL/HOLCF/IOA/ABP/Check.ML
    28.6      Author:     Olaf Mueller
    28.7  
    28.8  The Model Checker.
    29.1 --- a/src/HOL/HOLCF/IOA/ABP/Correctness.thy	Tue Mar 29 17:30:26 2011 +0200
    29.2 +++ b/src/HOL/HOLCF/IOA/ABP/Correctness.thy	Tue Mar 29 17:47:11 2011 +0200
    29.3 @@ -1,4 +1,4 @@
    29.4 -(*  Title:      HOLCF/IOA/ABP/Correctness.thy
    29.5 +(*  Title:      HOL/HOLCF/IOA/ABP/Correctness.thy
    29.6      Author:     Olaf Müller
    29.7  *)
    29.8  
    30.1 --- a/src/HOL/HOLCF/IOA/ABP/Env.thy	Tue Mar 29 17:30:26 2011 +0200
    30.2 +++ b/src/HOL/HOLCF/IOA/ABP/Env.thy	Tue Mar 29 17:47:11 2011 +0200
    30.3 @@ -1,4 +1,4 @@
    30.4 -(*  Title:      HOLCF/IOA/ABP/Impl.thy
    30.5 +(*  Title:      HOL/HOLCF/IOA/ABP/Env.thy
    30.6      Author:     Olaf Müller
    30.7  *)
    30.8  
    31.1 --- a/src/HOL/HOLCF/IOA/ABP/Impl.thy	Tue Mar 29 17:30:26 2011 +0200
    31.2 +++ b/src/HOL/HOLCF/IOA/ABP/Impl.thy	Tue Mar 29 17:47:11 2011 +0200
    31.3 @@ -1,4 +1,4 @@
    31.4 -(*  Title:      HOLCF/IOA/ABP/Impl.thy
    31.5 +(*  Title:      HOL/HOLCF/IOA/ABP/Impl.thy
    31.6      Author:     Olaf Müller
    31.7  *)
    31.8  
    32.1 --- a/src/HOL/HOLCF/IOA/ABP/Impl_finite.thy	Tue Mar 29 17:30:26 2011 +0200
    32.2 +++ b/src/HOL/HOLCF/IOA/ABP/Impl_finite.thy	Tue Mar 29 17:47:11 2011 +0200
    32.3 @@ -1,4 +1,4 @@
    32.4 -(*  Title:      HOLCF/IOA/ABP/Impl.thy
    32.5 +(*  Title:      HOL/HOLCF/IOA/ABP/Impl_finite.thy
    32.6      Author:     Olaf Müller
    32.7  *)
    32.8  
    33.1 --- a/src/HOL/HOLCF/IOA/ABP/Lemmas.thy	Tue Mar 29 17:30:26 2011 +0200
    33.2 +++ b/src/HOL/HOLCF/IOA/ABP/Lemmas.thy	Tue Mar 29 17:47:11 2011 +0200
    33.3 @@ -1,4 +1,4 @@
    33.4 -(*  Title:      HOLCF/IOA/ABP/Lemmas.thy
    33.5 +(*  Title:      HOL/HOLCF/IOA/ABP/Lemmas.thy
    33.6      Author:     Olaf Müller
    33.7  *)
    33.8  
    34.1 --- a/src/HOL/HOLCF/IOA/ABP/Packet.thy	Tue Mar 29 17:30:26 2011 +0200
    34.2 +++ b/src/HOL/HOLCF/IOA/ABP/Packet.thy	Tue Mar 29 17:47:11 2011 +0200
    34.3 @@ -1,4 +1,4 @@
    34.4 -(*  Title:      HOLCF/IOA/ABP/Packet.thy
    34.5 +(*  Title:      HOL/HOLCF/IOA/ABP/Packet.thy
    34.6      Author:     Olaf Müller
    34.7  *)
    34.8  
    35.1 --- a/src/HOL/HOLCF/IOA/ABP/ROOT.ML	Tue Mar 29 17:30:26 2011 +0200
    35.2 +++ b/src/HOL/HOLCF/IOA/ABP/ROOT.ML	Tue Mar 29 17:47:11 2011 +0200
    35.3 @@ -1,7 +1,8 @@
    35.4 -(*  Title:      HOLCF/IOA/ABP/ROOT.ML
    35.5 +(*  Title:      HOL/HOLCF/IOA/ABP/ROOT.ML
    35.6      Author:     Olaf Mueller
    35.7  
    35.8  This is the ROOT file for the Alternating Bit Protocol performed in
    35.9  I/O-Automata.
   35.10  *)
   35.11 +
   35.12  use_thys ["Correctness"];
    36.1 --- a/src/HOL/HOLCF/IOA/ABP/Receiver.thy	Tue Mar 29 17:30:26 2011 +0200
    36.2 +++ b/src/HOL/HOLCF/IOA/ABP/Receiver.thy	Tue Mar 29 17:47:11 2011 +0200
    36.3 @@ -1,4 +1,4 @@
    36.4 -(*  Title:      HOLCF/IOA/ABP/Receiver.thy
    36.5 +(*  Title:      HOL/HOLCF/IOA/ABP/Receiver.thy
    36.6      Author:     Olaf Müller
    36.7  *)
    36.8  
    37.1 --- a/src/HOL/HOLCF/IOA/ABP/Sender.thy	Tue Mar 29 17:30:26 2011 +0200
    37.2 +++ b/src/HOL/HOLCF/IOA/ABP/Sender.thy	Tue Mar 29 17:47:11 2011 +0200
    37.3 @@ -1,4 +1,4 @@
    37.4 -(*  Title:      HOLCF/IOA/ABP/Sender.thy
    37.5 +(*  Title:      HOL/HOLCF/IOA/ABP/Sender.thy
    37.6      Author:     Olaf Müller
    37.7  *)
    37.8  
    38.1 --- a/src/HOL/HOLCF/IOA/ABP/Spec.thy	Tue Mar 29 17:30:26 2011 +0200
    38.2 +++ b/src/HOL/HOLCF/IOA/ABP/Spec.thy	Tue Mar 29 17:47:11 2011 +0200
    38.3 @@ -1,4 +1,4 @@
    38.4 -(*  Title:      HOLCF/IOA/ABP/Spec.thy
    38.5 +(*  Title:      HOL/HOLCF/IOA/ABP/Spec.thy
    38.6      Author:     Olaf Müller
    38.7  *)
    38.8  
    39.1 --- a/src/HOL/HOLCF/IOA/NTP/Abschannel.thy	Tue Mar 29 17:30:26 2011 +0200
    39.2 +++ b/src/HOL/HOLCF/IOA/NTP/Abschannel.thy	Tue Mar 29 17:47:11 2011 +0200
    39.3 @@ -1,4 +1,4 @@
    39.4 -(*  Title:      HOL/IOA/NTP/Abschannel.thy
    39.5 +(*  Title:      HOL/HOLCF/IOA/NTP/Abschannel.thy
    39.6      Author:     Olaf Müller
    39.7  *)
    39.8  
    40.1 --- a/src/HOL/HOLCF/IOA/NTP/Action.thy	Tue Mar 29 17:30:26 2011 +0200
    40.2 +++ b/src/HOL/HOLCF/IOA/NTP/Action.thy	Tue Mar 29 17:47:11 2011 +0200
    40.3 @@ -1,4 +1,4 @@
    40.4 -(*  Title:      HOL/IOA/NTP/Action.thy
    40.5 +(*  Title:      HOL/HOLCF/IOA/NTP/Action.thy
    40.6      Author:     Tobias Nipkow & Konrad Slind
    40.7  *)
    40.8  
    41.1 --- a/src/HOL/HOLCF/IOA/NTP/Correctness.thy	Tue Mar 29 17:30:26 2011 +0200
    41.2 +++ b/src/HOL/HOLCF/IOA/NTP/Correctness.thy	Tue Mar 29 17:47:11 2011 +0200
    41.3 @@ -1,4 +1,4 @@
    41.4 -(*  Title:      HOL/IOA/NTP/Correctness.thy
    41.5 +(*  Title:      HOL/HOLCF/IOA/NTP/Correctness.thy
    41.6      Author:     Tobias Nipkow & Konrad Slind
    41.7  *)
    41.8  
    42.1 --- a/src/HOL/HOLCF/IOA/NTP/Impl.thy	Tue Mar 29 17:30:26 2011 +0200
    42.2 +++ b/src/HOL/HOLCF/IOA/NTP/Impl.thy	Tue Mar 29 17:47:11 2011 +0200
    42.3 @@ -1,4 +1,4 @@
    42.4 -(*  Title:      HOL/IOA/NTP/Impl.thy
    42.5 +(*  Title:      HOL/HOLCF/IOA/NTP/Impl.thy
    42.6      Author:     Tobias Nipkow & Konrad Slind
    42.7  *)
    42.8  
    43.1 --- a/src/HOL/HOLCF/IOA/NTP/Lemmas.thy	Tue Mar 29 17:30:26 2011 +0200
    43.2 +++ b/src/HOL/HOLCF/IOA/NTP/Lemmas.thy	Tue Mar 29 17:47:11 2011 +0200
    43.3 @@ -1,4 +1,4 @@
    43.4 -(*  Title:      HOL/IOA/NTP/Lemmas.thy
    43.5 +(*  Title:      HOL/HOLCF/IOA/NTP/Lemmas.thy
    43.6      Author:     Tobias Nipkow & Konrad Slind
    43.7  *)
    43.8  
    44.1 --- a/src/HOL/HOLCF/IOA/NTP/Multiset.thy	Tue Mar 29 17:30:26 2011 +0200
    44.2 +++ b/src/HOL/HOLCF/IOA/NTP/Multiset.thy	Tue Mar 29 17:47:11 2011 +0200
    44.3 @@ -1,4 +1,4 @@
    44.4 -(*  Title:      HOL/IOA/NTP/Multiset.thy
    44.5 +(*  Title:      HOL/HOLCF/IOA/NTP/Multiset.thy
    44.6      Author:     Tobias Nipkow & Konrad Slind
    44.7  *)
    44.8  
    45.1 --- a/src/HOL/HOLCF/IOA/NTP/Packet.thy	Tue Mar 29 17:30:26 2011 +0200
    45.2 +++ b/src/HOL/HOLCF/IOA/NTP/Packet.thy	Tue Mar 29 17:47:11 2011 +0200
    45.3 @@ -1,4 +1,4 @@
    45.4 -(*  Title:      HOL/IOA/NTP/Packet.thy
    45.5 +(*  Title:      HOL/HOLCF/IOA/NTP/Packet.thy
    45.6      Author:     Tobias Nipkow & Konrad Slind
    45.7  *)
    45.8  
    46.1 --- a/src/HOL/HOLCF/IOA/NTP/ROOT.ML	Tue Mar 29 17:30:26 2011 +0200
    46.2 +++ b/src/HOL/HOLCF/IOA/NTP/ROOT.ML	Tue Mar 29 17:47:11 2011 +0200
    46.3 @@ -1,4 +1,4 @@
    46.4 -(*  Title:      HOLCF/IOA/NTP/ROOT.ML
    46.5 +(*  Title:      HOL/HOLCF/IOA/NTP/ROOT.ML
    46.6      Author:     Tobias Nipkow & Konrad Slind
    46.7  
    46.8  This is the ROOT file for a network transmission protocol (NTP
    47.1 --- a/src/HOL/HOLCF/IOA/NTP/Receiver.thy	Tue Mar 29 17:30:26 2011 +0200
    47.2 +++ b/src/HOL/HOLCF/IOA/NTP/Receiver.thy	Tue Mar 29 17:47:11 2011 +0200
    47.3 @@ -1,4 +1,4 @@
    47.4 -(*  Title:      HOL/IOA/NTP/Receiver.thy
    47.5 +(*  Title:      HOL/HOLCF/IOA/NTP/Receiver.thy
    47.6      Author:     Tobias Nipkow & Konrad Slind
    47.7  *)
    47.8  
    48.1 --- a/src/HOL/HOLCF/IOA/NTP/Sender.thy	Tue Mar 29 17:30:26 2011 +0200
    48.2 +++ b/src/HOL/HOLCF/IOA/NTP/Sender.thy	Tue Mar 29 17:47:11 2011 +0200
    48.3 @@ -1,4 +1,4 @@
    48.4 -(*  Title:      HOL/IOA/NTP/Sender.thy
    48.5 +(*  Title:      HOL/HOLCF/IOA/NTP/Sender.thy
    48.6      Author:     Tobias Nipkow & Konrad Slind
    48.7  *)
    48.8  
    49.1 --- a/src/HOL/HOLCF/IOA/NTP/Spec.thy	Tue Mar 29 17:30:26 2011 +0200
    49.2 +++ b/src/HOL/HOLCF/IOA/NTP/Spec.thy	Tue Mar 29 17:47:11 2011 +0200
    49.3 @@ -1,4 +1,4 @@
    49.4 -(*  Title:      HOL/IOA/NTP/Spec.thy
    49.5 +(*  Title:      HOL/HOLCF/IOA/NTP/Spec.thy
    49.6      Author:     Tobias Nipkow & Konrad Slind
    49.7  *)
    49.8  
    50.1 --- a/src/HOL/HOLCF/IOA/ROOT.ML	Tue Mar 29 17:30:26 2011 +0200
    50.2 +++ b/src/HOL/HOLCF/IOA/ROOT.ML	Tue Mar 29 17:47:11 2011 +0200
    50.3 @@ -1,4 +1,4 @@
    50.4 -(*  Title:      HOLCF/IOA/ROOT.ML
    50.5 +(*  Title:      HOL/HOLCF/IOA/ROOT.ML
    50.6      Author:     Olaf Mueller
    50.7  
    50.8  Formalization of a semantic model of I/O-Automata.  See README.html
    51.1 --- a/src/HOL/HOLCF/IOA/Storage/Action.thy	Tue Mar 29 17:30:26 2011 +0200
    51.2 +++ b/src/HOL/HOLCF/IOA/Storage/Action.thy	Tue Mar 29 17:47:11 2011 +0200
    51.3 @@ -1,4 +1,4 @@
    51.4 -(*  Title:      HOLCF/IOA/ABP/Action.thy
    51.5 +(*  Title:      HOL/HOLCF/IOA/Storage/Action.thy
    51.6      Author:     Olaf Müller
    51.7  *)
    51.8  
    52.1 --- a/src/HOL/HOLCF/IOA/Storage/Correctness.thy	Tue Mar 29 17:30:26 2011 +0200
    52.2 +++ b/src/HOL/HOLCF/IOA/Storage/Correctness.thy	Tue Mar 29 17:47:11 2011 +0200
    52.3 @@ -1,4 +1,4 @@
    52.4 -(*  Title:      HOL/IOA/example/Correctness.thy
    52.5 +(*  Title:      HOL/HOLCF/IOA/Storage/Correctness.thy
    52.6      Author:     Olaf Müller
    52.7  *)
    52.8  
    53.1 --- a/src/HOL/HOLCF/IOA/Storage/Impl.thy	Tue Mar 29 17:30:26 2011 +0200
    53.2 +++ b/src/HOL/HOLCF/IOA/Storage/Impl.thy	Tue Mar 29 17:47:11 2011 +0200
    53.3 @@ -1,4 +1,4 @@
    53.4 -(*  Title:      HOL/IOA/example/Spec.thy
    53.5 +(*  Title:      HOL/HOLCF/IOA/Storage/Impl.thy
    53.6      Author:     Olaf Müller
    53.7  *)
    53.8  
    54.1 --- a/src/HOL/HOLCF/IOA/Storage/ROOT.ML	Tue Mar 29 17:30:26 2011 +0200
    54.2 +++ b/src/HOL/HOLCF/IOA/Storage/ROOT.ML	Tue Mar 29 17:47:11 2011 +0200
    54.3 @@ -1,4 +1,4 @@
    54.4 -(*  Title:      HOLCF/IOA/Storage/ROOT.ML
    54.5 +(*  Title:      HOL/HOLCF/IOA/Storage/ROOT.ML
    54.6      Author:     Olaf Mueller
    54.7  
    54.8  Memory storage case study.
    55.1 --- a/src/HOL/HOLCF/IOA/Storage/Spec.thy	Tue Mar 29 17:30:26 2011 +0200
    55.2 +++ b/src/HOL/HOLCF/IOA/Storage/Spec.thy	Tue Mar 29 17:47:11 2011 +0200
    55.3 @@ -1,4 +1,4 @@
    55.4 -(*  Title:      HOL/IOA/example/Spec.thy
    55.5 +(*  Title:      HOL/HOLCF/IOA/Storage/Spec.thy
    55.6      Author:     Olaf Müller
    55.7  *)
    55.8  
    56.1 --- a/src/HOL/HOLCF/IOA/ex/ROOT.ML	Tue Mar 29 17:30:26 2011 +0200
    56.2 +++ b/src/HOL/HOLCF/IOA/ex/ROOT.ML	Tue Mar 29 17:47:11 2011 +0200
    56.3 @@ -1,4 +1,4 @@
    56.4 -(*  Title:      HOLCF/IOA/ex/ROOT.ML
    56.5 +(*  Title:      HOL/HOLCF/IOA/ex/ROOT.ML
    56.6      Author:     Olaf Mueller
    56.7  *)
    56.8  
    57.1 --- a/src/HOL/HOLCF/IOA/ex/TrivEx.thy	Tue Mar 29 17:30:26 2011 +0200
    57.2 +++ b/src/HOL/HOLCF/IOA/ex/TrivEx.thy	Tue Mar 29 17:47:11 2011 +0200
    57.3 @@ -1,4 +1,4 @@
    57.4 -(*  Title:      HOLCF/IOA/TrivEx.thy
    57.5 +(*  Title:      HOL/HOLCF/IOA/ex/TrivEx.thy
    57.6      Author:     Olaf Müller
    57.7  *)
    57.8  
    58.1 --- a/src/HOL/HOLCF/IOA/ex/TrivEx2.thy	Tue Mar 29 17:30:26 2011 +0200
    58.2 +++ b/src/HOL/HOLCF/IOA/ex/TrivEx2.thy	Tue Mar 29 17:47:11 2011 +0200
    58.3 @@ -1,4 +1,4 @@
    58.4 -(*  Title:      HOLCF/IOA/TrivEx.thy
    58.5 +(*  Title:      HOL/HOLCF/IOA/ex/TrivEx2.thy
    58.6      Author:     Olaf Müller
    58.7  *)
    58.8  
    59.1 --- a/src/HOL/HOLCF/IOA/meta_theory/Abstraction.thy	Tue Mar 29 17:30:26 2011 +0200
    59.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/Abstraction.thy	Tue Mar 29 17:47:11 2011 +0200
    59.3 @@ -1,4 +1,4 @@
    59.4 -(*  Title:      HOLCF/IOA/meta_theory/Abstraction.thy
    59.5 +(*  Title:      HOL/HOLCF/IOA/meta_theory/Abstraction.thy
    59.6      Author:     Olaf Müller
    59.7  *)
    59.8  
    60.1 --- a/src/HOL/HOLCF/IOA/meta_theory/Asig.thy	Tue Mar 29 17:30:26 2011 +0200
    60.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/Asig.thy	Tue Mar 29 17:47:11 2011 +0200
    60.3 @@ -1,4 +1,4 @@
    60.4 -(*  Title:      HOL/IOA/meta_theory/Asig.thy
    60.5 +(*  Title:      HOL/HOLCF/IOA/meta_theory/Asig.thy
    60.6      Author:     Olaf Müller, Tobias Nipkow & Konrad Slind
    60.7  *)
    60.8  
    61.1 --- a/src/HOL/HOLCF/IOA/meta_theory/Automata.thy	Tue Mar 29 17:30:26 2011 +0200
    61.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/Automata.thy	Tue Mar 29 17:47:11 2011 +0200
    61.3 @@ -1,4 +1,4 @@
    61.4 -(*  Title:      HOLCF/IOA/meta_theory/Automata.thy
    61.5 +(*  Title:      HOL/HOLCF/IOA/meta_theory/Automata.thy
    61.6      Author:     Olaf Müller, Konrad Slind, Tobias Nipkow
    61.7  *)
    61.8  
    62.1 --- a/src/HOL/HOLCF/IOA/meta_theory/CompoExecs.thy	Tue Mar 29 17:30:26 2011 +0200
    62.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/CompoExecs.thy	Tue Mar 29 17:47:11 2011 +0200
    62.3 @@ -1,4 +1,4 @@
    62.4 -(*  Title:      HOLCF/IOA/meta_theory/CompoExecs.thy
    62.5 +(*  Title:      HOL/HOLCF/IOA/meta_theory/CompoExecs.thy
    62.6      Author:     Olaf Müller
    62.7  *)
    62.8  
    63.1 --- a/src/HOL/HOLCF/IOA/meta_theory/CompoScheds.thy	Tue Mar 29 17:30:26 2011 +0200
    63.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/CompoScheds.thy	Tue Mar 29 17:47:11 2011 +0200
    63.3 @@ -1,4 +1,4 @@
    63.4 -(*  Title:      HOLCF/IOA/meta_theory/CompoScheds.thy
    63.5 +(*  Title:      HOL/HOLCF/IOA/meta_theory/CompoScheds.thy
    63.6      Author:     Olaf Müller
    63.7  *)
    63.8  
    64.1 --- a/src/HOL/HOLCF/IOA/meta_theory/CompoTraces.thy	Tue Mar 29 17:30:26 2011 +0200
    64.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/CompoTraces.thy	Tue Mar 29 17:47:11 2011 +0200
    64.3 @@ -1,4 +1,4 @@
    64.4 -(*  Title:      HOLCF/IOA/meta_theory/CompoTraces.thy
    64.5 +(*  Title:      HOL/HOLCF/IOA/meta_theory/CompoTraces.thy
    64.6      Author:     Olaf Müller
    64.7  *) 
    64.8  
    65.1 --- a/src/HOL/HOLCF/IOA/meta_theory/Compositionality.thy	Tue Mar 29 17:30:26 2011 +0200
    65.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/Compositionality.thy	Tue Mar 29 17:47:11 2011 +0200
    65.3 @@ -1,4 +1,4 @@
    65.4 -(*  Title:      HOLCF/IOA/meta_theory/Compositionality.thy
    65.5 +(*  Title:      HOL/HOLCF/IOA/meta_theory/Compositionality.thy
    65.6      Author:     Olaf Müller
    65.7  *)
    65.8  
    66.1 --- a/src/HOL/HOLCF/IOA/meta_theory/Deadlock.thy	Tue Mar 29 17:30:26 2011 +0200
    66.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/Deadlock.thy	Tue Mar 29 17:47:11 2011 +0200
    66.3 @@ -1,4 +1,4 @@
    66.4 -(*  Title:      HOLCF/IOA/meta_theory/Deadlock.thy
    66.5 +(*  Title:      HOL/HOLCF/IOA/meta_theory/Deadlock.thy
    66.6      Author:     Olaf Müller
    66.7  *)
    66.8  
    67.1 --- a/src/HOL/HOLCF/IOA/meta_theory/IOA.thy	Tue Mar 29 17:30:26 2011 +0200
    67.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/IOA.thy	Tue Mar 29 17:47:11 2011 +0200
    67.3 @@ -1,4 +1,4 @@
    67.4 -(*  Title:      HOLCF/IOA/meta_theory/IOA.thy
    67.5 +(*  Title:      HOL/HOLCF/IOA/meta_theory/IOA.thy
    67.6      Author:     Olaf Müller
    67.7  *)
    67.8  
    68.1 --- a/src/HOL/HOLCF/IOA/meta_theory/LiveIOA.thy	Tue Mar 29 17:30:26 2011 +0200
    68.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/LiveIOA.thy	Tue Mar 29 17:47:11 2011 +0200
    68.3 @@ -1,4 +1,4 @@
    68.4 -(*  Title:      HOLCF/IOA/meta_theory/LiveIOA.thy
    68.5 +(*  Title:      HOL/HOLCF/IOA/meta_theory/LiveIOA.thy
    68.6      Author:     Olaf Müller
    68.7  *)
    68.8  
    69.1 --- a/src/HOL/HOLCF/IOA/meta_theory/Pred.thy	Tue Mar 29 17:30:26 2011 +0200
    69.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/Pred.thy	Tue Mar 29 17:47:11 2011 +0200
    69.3 @@ -1,4 +1,4 @@
    69.4 -(*  Title:      HOLCF/IOA/meta_theory/Pred.thy
    69.5 +(*  Title:      HOL/HOLCF/IOA/meta_theory/Pred.thy
    69.6      Author:     Olaf Müller
    69.7  *)
    69.8  
    70.1 --- a/src/HOL/HOLCF/IOA/meta_theory/RefCorrectness.thy	Tue Mar 29 17:30:26 2011 +0200
    70.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/RefCorrectness.thy	Tue Mar 29 17:47:11 2011 +0200
    70.3 @@ -1,4 +1,4 @@
    70.4 -(*  Title:      HOLCF/IOA/meta_theory/RefCorrectness.thy
    70.5 +(*  Title:      HOL/HOLCF/IOA/meta_theory/RefCorrectness.thy
    70.6      Author:     Olaf Müller
    70.7  *)
    70.8  
    71.1 --- a/src/HOL/HOLCF/IOA/meta_theory/RefMappings.thy	Tue Mar 29 17:30:26 2011 +0200
    71.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/RefMappings.thy	Tue Mar 29 17:47:11 2011 +0200
    71.3 @@ -1,4 +1,4 @@
    71.4 -(*  Title:      HOLCF/IOA/meta_theory/RefMappings.thy
    71.5 +(*  Title:      HOL/HOLCF/IOA/meta_theory/RefMappings.thy
    71.6      Author:     Olaf Müller
    71.7  *)
    71.8  
    72.1 --- a/src/HOL/HOLCF/IOA/meta_theory/Seq.thy	Tue Mar 29 17:30:26 2011 +0200
    72.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/Seq.thy	Tue Mar 29 17:47:11 2011 +0200
    72.3 @@ -1,4 +1,4 @@
    72.4 -(*  Title:      HOLCF/IOA/meta_theory/Seq.thy
    72.5 +(*  Title:      HOL/HOLCF/IOA/meta_theory/Seq.thy
    72.6      Author:     Olaf Müller
    72.7  *)
    72.8  
    73.1 --- a/src/HOL/HOLCF/IOA/meta_theory/Sequence.thy	Tue Mar 29 17:30:26 2011 +0200
    73.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/Sequence.thy	Tue Mar 29 17:47:11 2011 +0200
    73.3 @@ -1,4 +1,4 @@
    73.4 -(*  Title:      HOLCF/IOA/meta_theory/Sequence.thy
    73.5 +(*  Title:      HOL/HOLCF/IOA/meta_theory/Sequence.thy
    73.6      Author:     Olaf Müller
    73.7  
    73.8  Sequences over flat domains with lifted elements.
    74.1 --- a/src/HOL/HOLCF/IOA/meta_theory/ShortExecutions.thy	Tue Mar 29 17:30:26 2011 +0200
    74.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/ShortExecutions.thy	Tue Mar 29 17:47:11 2011 +0200
    74.3 @@ -1,4 +1,4 @@
    74.4 -(*  Title:      HOLCF/IOA/meta_theory/ShortExecutions.thy
    74.5 +(*  Title:      HOL/HOLCF/IOA/meta_theory/ShortExecutions.thy
    74.6      Author:     Olaf Müller
    74.7  *)
    74.8  
    75.1 --- a/src/HOL/HOLCF/IOA/meta_theory/SimCorrectness.thy	Tue Mar 29 17:30:26 2011 +0200
    75.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/SimCorrectness.thy	Tue Mar 29 17:47:11 2011 +0200
    75.3 @@ -1,4 +1,4 @@
    75.4 -(*  Title:      HOLCF/IOA/meta_theory/SimCorrectness.thy
    75.5 +(*  Title:      HOL/HOLCF/IOA/meta_theory/SimCorrectness.thy
    75.6      Author:     Olaf Müller
    75.7  *)
    75.8  
    76.1 --- a/src/HOL/HOLCF/IOA/meta_theory/Simulations.thy	Tue Mar 29 17:30:26 2011 +0200
    76.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/Simulations.thy	Tue Mar 29 17:47:11 2011 +0200
    76.3 @@ -1,4 +1,4 @@
    76.4 -(*  Title:      HOLCF/IOA/meta_theory/Simulations.thy
    76.5 +(*  Title:      HOL/HOLCF/IOA/meta_theory/Simulations.thy
    76.6      Author:     Olaf Müller
    76.7  *)
    76.8  
    77.1 --- a/src/HOL/HOLCF/IOA/meta_theory/TL.thy	Tue Mar 29 17:30:26 2011 +0200
    77.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/TL.thy	Tue Mar 29 17:47:11 2011 +0200
    77.3 @@ -1,4 +1,4 @@
    77.4 -(*  Title:      HOLCF/IOA/meta_theory/TLS.thy
    77.5 +(*  Title:      HOL/HOLCF/IOA/meta_theory/TL.thy
    77.6      Author:     Olaf Müller
    77.7  *)
    77.8  
    78.1 --- a/src/HOL/HOLCF/IOA/meta_theory/TLS.thy	Tue Mar 29 17:30:26 2011 +0200
    78.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/TLS.thy	Tue Mar 29 17:47:11 2011 +0200
    78.3 @@ -1,4 +1,4 @@
    78.4 -(*  Title:      HOLCF/IOA/meta_theory/TLS.thy
    78.5 +(*  Title:      HOL/HOLCF/IOA/meta_theory/TLS.thy
    78.6      Author:     Olaf Müller
    78.7  *)
    78.8  
    79.1 --- a/src/HOL/HOLCF/IOA/meta_theory/Traces.thy	Tue Mar 29 17:30:26 2011 +0200
    79.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/Traces.thy	Tue Mar 29 17:47:11 2011 +0200
    79.3 @@ -1,4 +1,4 @@
    79.4 -(*  Title:      HOLCF/IOA/meta_theory/Traces.thy
    79.5 +(*  Title:      HOL/HOLCF/IOA/meta_theory/Traces.thy
    79.6      Author:     Olaf Müller
    79.7  *)
    79.8  
    80.1 --- a/src/HOL/HOLCF/Library/Bool_Discrete.thy	Tue Mar 29 17:30:26 2011 +0200
    80.2 +++ b/src/HOL/HOLCF/Library/Bool_Discrete.thy	Tue Mar 29 17:47:11 2011 +0200
    80.3 @@ -1,4 +1,4 @@
    80.4 -(*  Title:      HOLCF/Library/Bool_Discrete.thy
    80.5 +(*  Title:      HOL/HOLCF/Library/Bool_Discrete.thy
    80.6      Author:     Brian Huffman
    80.7  *)
    80.8  
    81.1 --- a/src/HOL/HOLCF/Library/Char_Discrete.thy	Tue Mar 29 17:30:26 2011 +0200
    81.2 +++ b/src/HOL/HOLCF/Library/Char_Discrete.thy	Tue Mar 29 17:47:11 2011 +0200
    81.3 @@ -1,4 +1,4 @@
    81.4 -(*  Title:      HOLCF/Library/Char_Discrete.thy
    81.5 +(*  Title:      HOL/HOLCF/Library/Char_Discrete.thy
    81.6      Author:     Brian Huffman
    81.7  *)
    81.8  
    82.1 --- a/src/HOL/HOLCF/Library/Defl_Bifinite.thy	Tue Mar 29 17:30:26 2011 +0200
    82.2 +++ b/src/HOL/HOLCF/Library/Defl_Bifinite.thy	Tue Mar 29 17:47:11 2011 +0200
    82.3 @@ -1,4 +1,4 @@
    82.4 -(*  Title:      HOLCF/Library/Defl_Bifinite.thy
    82.5 +(*  Title:      HOL/HOLCF/Library/Defl_Bifinite.thy
    82.6      Author:     Brian Huffman
    82.7  *)
    82.8  
    83.1 --- a/src/HOL/HOLCF/Library/HOL_Cpo.thy	Tue Mar 29 17:30:26 2011 +0200
    83.2 +++ b/src/HOL/HOLCF/Library/HOL_Cpo.thy	Tue Mar 29 17:47:11 2011 +0200
    83.3 @@ -1,4 +1,4 @@
    83.4 -(*  Title:      HOLCF/HOL_Cpo.thy
    83.5 +(*  Title:      HOL/HOLCF/Library/HOL_Cpo.thy
    83.6      Author:     Brian Huffman
    83.7  *)
    83.8  
    84.1 --- a/src/HOL/HOLCF/Library/Int_Discrete.thy	Tue Mar 29 17:30:26 2011 +0200
    84.2 +++ b/src/HOL/HOLCF/Library/Int_Discrete.thy	Tue Mar 29 17:47:11 2011 +0200
    84.3 @@ -1,4 +1,4 @@
    84.4 -(*  Title:      HOLCF/Library/Int_Discrete.thy
    84.5 +(*  Title:      HOL/HOLCF/Library/Int_Discrete.thy
    84.6      Author:     Brian Huffman
    84.7  *)
    84.8  
    85.1 --- a/src/HOL/HOLCF/Library/List_Cpo.thy	Tue Mar 29 17:30:26 2011 +0200
    85.2 +++ b/src/HOL/HOLCF/Library/List_Cpo.thy	Tue Mar 29 17:47:11 2011 +0200
    85.3 @@ -1,4 +1,4 @@
    85.4 -(*  Title:      HOLCF/Library/List_Cpo.thy
    85.5 +(*  Title:      HOL/HOLCF/Library/List_Cpo.thy
    85.6      Author:     Brian Huffman
    85.7  *)
    85.8  
    86.1 --- a/src/HOL/HOLCF/Library/List_Predomain.thy	Tue Mar 29 17:30:26 2011 +0200
    86.2 +++ b/src/HOL/HOLCF/Library/List_Predomain.thy	Tue Mar 29 17:47:11 2011 +0200
    86.3 @@ -1,4 +1,4 @@
    86.4 -(*  Title:      HOLCF/Library/List_Predomain.thy
    86.5 +(*  Title:      HOL/HOLCF/Library/List_Predomain.thy
    86.6      Author:     Brian Huffman
    86.7  *)
    86.8  
    87.1 --- a/src/HOL/HOLCF/Library/Nat_Discrete.thy	Tue Mar 29 17:30:26 2011 +0200
    87.2 +++ b/src/HOL/HOLCF/Library/Nat_Discrete.thy	Tue Mar 29 17:47:11 2011 +0200
    87.3 @@ -1,4 +1,4 @@
    87.4 -(*  Title:      HOLCF/Library/Nat_Discrete.thy
    87.5 +(*  Title:      HOL/HOLCF/Library/Nat_Discrete.thy
    87.6      Author:     Brian Huffman
    87.7  *)
    87.8  
    88.1 --- a/src/HOL/HOLCF/Library/Option_Cpo.thy	Tue Mar 29 17:30:26 2011 +0200
    88.2 +++ b/src/HOL/HOLCF/Library/Option_Cpo.thy	Tue Mar 29 17:47:11 2011 +0200
    88.3 @@ -1,4 +1,4 @@
    88.4 -(*  Title:      HOLCF/Option_Cpo.thy
    88.5 +(*  Title:      HOL/HOLCF/Library/Option_Cpo.thy
    88.6      Author:     Brian Huffman
    88.7  *)
    88.8  
    89.1 --- a/src/HOL/HOLCF/Library/Stream.thy	Tue Mar 29 17:30:26 2011 +0200
    89.2 +++ b/src/HOL/HOLCF/Library/Stream.thy	Tue Mar 29 17:47:11 2011 +0200
    89.3 @@ -1,4 +1,4 @@
    89.4 -(*  Title:      HOLCF/ex/Stream.thy
    89.5 +(*  Title:      HOL/HOLCF/Library/Stream.thy
    89.6      Author:     Franz Regensburger, David von Oheimb, Borislav Gajanovic
    89.7  *)
    89.8  
    90.1 --- a/src/HOL/HOLCF/Library/Sum_Cpo.thy	Tue Mar 29 17:30:26 2011 +0200
    90.2 +++ b/src/HOL/HOLCF/Library/Sum_Cpo.thy	Tue Mar 29 17:47:11 2011 +0200
    90.3 @@ -1,4 +1,4 @@
    90.4 -(*  Title:      HOLCF/Sum_Cpo.thy
    90.5 +(*  Title:      HOL/HOLCF/Library/Sum_Cpo.thy
    90.6      Author:     Brian Huffman
    90.7  *)
    90.8  
    91.1 --- a/src/HOL/HOLCF/Lift.thy	Tue Mar 29 17:30:26 2011 +0200
    91.2 +++ b/src/HOL/HOLCF/Lift.thy	Tue Mar 29 17:47:11 2011 +0200
    91.3 @@ -1,4 +1,4 @@
    91.4 -(*  Title:      HOLCF/Lift.thy
    91.5 +(*  Title:      HOL/HOLCF/Lift.thy
    91.6      Author:     Olaf Mueller
    91.7  *)
    91.8  
    92.1 --- a/src/HOL/HOLCF/LowerPD.thy	Tue Mar 29 17:30:26 2011 +0200
    92.2 +++ b/src/HOL/HOLCF/LowerPD.thy	Tue Mar 29 17:47:11 2011 +0200
    92.3 @@ -1,4 +1,4 @@
    92.4 -(*  Title:      HOLCF/LowerPD.thy
    92.5 +(*  Title:      HOL/HOLCF/LowerPD.thy
    92.6      Author:     Brian Huffman
    92.7  *)
    92.8  
    93.1 --- a/src/HOL/HOLCF/Map_Functions.thy	Tue Mar 29 17:30:26 2011 +0200
    93.2 +++ b/src/HOL/HOLCF/Map_Functions.thy	Tue Mar 29 17:47:11 2011 +0200
    93.3 @@ -1,4 +1,4 @@
    93.4 -(*  Title:      HOLCF/Map_Functions.thy
    93.5 +(*  Title:      HOL/HOLCF/Map_Functions.thy
    93.6      Author:     Brian Huffman
    93.7  *)
    93.8  
    94.1 --- a/src/HOL/HOLCF/One.thy	Tue Mar 29 17:30:26 2011 +0200
    94.2 +++ b/src/HOL/HOLCF/One.thy	Tue Mar 29 17:47:11 2011 +0200
    94.3 @@ -1,4 +1,4 @@
    94.4 -(*  Title:      HOLCF/One.thy
    94.5 +(*  Title:      HOL/HOLCF/One.thy
    94.6      Author:     Oscar Slotosch
    94.7  *)
    94.8  
    95.1 --- a/src/HOL/HOLCF/Pcpo.thy	Tue Mar 29 17:30:26 2011 +0200
    95.2 +++ b/src/HOL/HOLCF/Pcpo.thy	Tue Mar 29 17:47:11 2011 +0200
    95.3 @@ -1,4 +1,4 @@
    95.4 -(*  Title:      HOLCF/Pcpo.thy
    95.5 +(*  Title:      HOL/HOLCF/Pcpo.thy
    95.6      Author:     Franz Regensburger
    95.7  *)
    95.8  
    96.1 --- a/src/HOL/HOLCF/Plain_HOLCF.thy	Tue Mar 29 17:30:26 2011 +0200
    96.2 +++ b/src/HOL/HOLCF/Plain_HOLCF.thy	Tue Mar 29 17:47:11 2011 +0200
    96.3 @@ -1,4 +1,4 @@
    96.4 -(*  Title:      HOLCF/Plain_HOLCF.thy
    96.5 +(*  Title:      HOL/HOLCF/Plain_HOLCF.thy
    96.6      Author:     Brian Huffman
    96.7  *)
    96.8  
    97.1 --- a/src/HOL/HOLCF/Porder.thy	Tue Mar 29 17:30:26 2011 +0200
    97.2 +++ b/src/HOL/HOLCF/Porder.thy	Tue Mar 29 17:47:11 2011 +0200
    97.3 @@ -1,4 +1,4 @@
    97.4 -(*  Title:      HOLCF/Porder.thy
    97.5 +(*  Title:      HOL/HOLCF/Porder.thy
    97.6      Author:     Franz Regensburger and Brian Huffman
    97.7  *)
    97.8  
    98.1 --- a/src/HOL/HOLCF/Powerdomains.thy	Tue Mar 29 17:30:26 2011 +0200
    98.2 +++ b/src/HOL/HOLCF/Powerdomains.thy	Tue Mar 29 17:47:11 2011 +0200
    98.3 @@ -1,4 +1,4 @@
    98.4 -(*  Title:      HOLCF/Powerdomains.thy
    98.5 +(*  Title:      HOL/HOLCF/Powerdomains.thy
    98.6      Author:     Brian Huffman
    98.7  *)
    98.8  
    99.1 --- a/src/HOL/HOLCF/Product_Cpo.thy	Tue Mar 29 17:30:26 2011 +0200
    99.2 +++ b/src/HOL/HOLCF/Product_Cpo.thy	Tue Mar 29 17:47:11 2011 +0200
    99.3 @@ -1,4 +1,4 @@
    99.4 -(*  Title:      HOLCF/Product_Cpo.thy
    99.5 +(*  Title:      HOL/HOLCF/Product_Cpo.thy
    99.6      Author:     Franz Regensburger
    99.7  *)
    99.8  
   100.1 --- a/src/HOL/HOLCF/ROOT.ML	Tue Mar 29 17:30:26 2011 +0200
   100.2 +++ b/src/HOL/HOLCF/ROOT.ML	Tue Mar 29 17:47:11 2011 +0200
   100.3 @@ -1,4 +1,4 @@
   100.4 -(*  Title:      HOLCF/ROOT.ML
   100.5 +(*  Title:      HOL/HOLCF/ROOT.ML
   100.6      Author:     Franz Regensburger
   100.7  
   100.8  HOLCF -- a semantic extension of HOL by the LCF logic.
   101.1 --- a/src/HOL/HOLCF/Representable.thy	Tue Mar 29 17:30:26 2011 +0200
   101.2 +++ b/src/HOL/HOLCF/Representable.thy	Tue Mar 29 17:47:11 2011 +0200
   101.3 @@ -1,4 +1,4 @@
   101.4 -(*  Title:      HOLCF/Representable.thy
   101.5 +(*  Title:      HOL/HOLCF/Representable.thy
   101.6      Author:     Brian Huffman
   101.7  *)
   101.8  
   102.1 --- a/src/HOL/HOLCF/Sfun.thy	Tue Mar 29 17:30:26 2011 +0200
   102.2 +++ b/src/HOL/HOLCF/Sfun.thy	Tue Mar 29 17:47:11 2011 +0200
   102.3 @@ -1,4 +1,4 @@
   102.4 -(*  Title:      HOLCF/Sfun.thy
   102.5 +(*  Title:      HOL/HOLCF/Sfun.thy
   102.6      Author:     Brian Huffman
   102.7  *)
   102.8  
   103.1 --- a/src/HOL/HOLCF/Sprod.thy	Tue Mar 29 17:30:26 2011 +0200
   103.2 +++ b/src/HOL/HOLCF/Sprod.thy	Tue Mar 29 17:47:11 2011 +0200
   103.3 @@ -1,4 +1,4 @@
   103.4 -(*  Title:      HOLCF/Sprod.thy
   103.5 +(*  Title:      HOL/HOLCF/Sprod.thy
   103.6      Author:     Franz Regensburger
   103.7      Author:     Brian Huffman
   103.8  *)
   104.1 --- a/src/HOL/HOLCF/Ssum.thy	Tue Mar 29 17:30:26 2011 +0200
   104.2 +++ b/src/HOL/HOLCF/Ssum.thy	Tue Mar 29 17:47:11 2011 +0200
   104.3 @@ -1,4 +1,4 @@
   104.4 -(*  Title:      HOLCF/Ssum.thy
   104.5 +(*  Title:      HOL/HOLCF/Ssum.thy
   104.6      Author:     Franz Regensburger
   104.7      Author:     Brian Huffman
   104.8  *)
   105.1 --- a/src/HOL/HOLCF/Tools/Domain/domain.ML	Tue Mar 29 17:30:26 2011 +0200
   105.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain.ML	Tue Mar 29 17:47:11 2011 +0200
   105.3 @@ -1,4 +1,4 @@
   105.4 -(*  Title:      HOLCF/Tools/Domain/domain.ML
   105.5 +(*  Title:      HOL/HOLCF/Tools/Domain/domain.ML
   105.6      Author:     David von Oheimb
   105.7      Author:     Brian Huffman
   105.8  
   106.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_axioms.ML	Tue Mar 29 17:30:26 2011 +0200
   106.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_axioms.ML	Tue Mar 29 17:47:11 2011 +0200
   106.3 @@ -1,4 +1,4 @@
   106.4 -(*  Title:      HOLCF/Tools/Domain/domain_axioms.ML
   106.5 +(*  Title:      HOL/HOLCF/Tools/Domain/domain_axioms.ML
   106.6      Author:     David von Oheimb
   106.7      Author:     Brian Huffman
   106.8  
   107.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML	Tue Mar 29 17:30:26 2011 +0200
   107.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML	Tue Mar 29 17:47:11 2011 +0200
   107.3 @@ -1,4 +1,4 @@
   107.4 -(*  Title:      HOLCF/Tools/Domain/domain_constructors.ML
   107.5 +(*  Title:      HOL/HOLCF/Tools/Domain/domain_constructors.ML
   107.6      Author:     Brian Huffman
   107.7  
   107.8  Defines constructor functions for a given domain isomorphism
   108.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_induction.ML	Tue Mar 29 17:30:26 2011 +0200
   108.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_induction.ML	Tue Mar 29 17:47:11 2011 +0200
   108.3 @@ -1,4 +1,4 @@
   108.4 -(*  Title:      HOLCF/Tools/Domain/domain_induction.ML
   108.5 +(*  Title:      HOL/HOLCF/Tools/Domain/domain_induction.ML
   108.6      Author:     David von Oheimb
   108.7      Author:     Brian Huffman
   108.8  
   109.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Tue Mar 29 17:30:26 2011 +0200
   109.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Tue Mar 29 17:47:11 2011 +0200
   109.3 @@ -1,4 +1,4 @@
   109.4 -(*  Title:      HOLCF/Tools/Domain/domain_isomorphism.ML
   109.5 +(*  Title:      HOL/HOLCF/Tools/Domain/domain_isomorphism.ML
   109.6      Author:     Brian Huffman
   109.7  
   109.8  Defines new types satisfying the given domain equations.
   110.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML	Tue Mar 29 17:30:26 2011 +0200
   110.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML	Tue Mar 29 17:47:11 2011 +0200
   110.3 @@ -1,4 +1,4 @@
   110.4 -(*  Title:      HOLCF/Tools/Domain/domain_take_proofs.ML
   110.5 +(*  Title:      HOL/HOLCF/Tools/Domain/domain_take_proofs.ML
   110.6      Author:     Brian Huffman
   110.7  
   110.8  Defines take functions for the given domain equation
   111.1 --- a/src/HOL/HOLCF/Tools/cont_consts.ML	Tue Mar 29 17:30:26 2011 +0200
   111.2 +++ b/src/HOL/HOLCF/Tools/cont_consts.ML	Tue Mar 29 17:47:11 2011 +0200
   111.3 @@ -1,4 +1,4 @@
   111.4 -(*  Title:      HOLCF/Tools/cont_consts.ML
   111.5 +(*  Title:      HOL/HOLCF/Tools/cont_consts.ML
   111.6      Author:     Tobias Mayr, David von Oheimb, and Markus Wenzel
   111.7  
   111.8  HOLCF version of consts: handle continuous function types in mixfix
   112.1 --- a/src/HOL/HOLCF/Tools/cont_proc.ML	Tue Mar 29 17:30:26 2011 +0200
   112.2 +++ b/src/HOL/HOLCF/Tools/cont_proc.ML	Tue Mar 29 17:47:11 2011 +0200
   112.3 @@ -1,4 +1,4 @@
   112.4 -(*  Title:      HOLCF/Tools/cont_proc.ML
   112.5 +(*  Title:      HOL/HOLCF/Tools/cont_proc.ML
   112.6      Author:     Brian Huffman
   112.7  *)
   112.8  
   113.1 --- a/src/HOL/HOLCF/Tools/cpodef.ML	Tue Mar 29 17:30:26 2011 +0200
   113.2 +++ b/src/HOL/HOLCF/Tools/cpodef.ML	Tue Mar 29 17:47:11 2011 +0200
   113.3 @@ -1,4 +1,4 @@
   113.4 -(*  Title:      HOLCF/Tools/cpodef.ML
   113.5 +(*  Title:      HOL/HOLCF/Tools/cpodef.ML
   113.6      Author:     Brian Huffman
   113.7  
   113.8  Primitive domain definitions for HOLCF, similar to Gordon/HOL-style
   114.1 --- a/src/HOL/HOLCF/Tools/domaindef.ML	Tue Mar 29 17:30:26 2011 +0200
   114.2 +++ b/src/HOL/HOLCF/Tools/domaindef.ML	Tue Mar 29 17:47:11 2011 +0200
   114.3 @@ -1,4 +1,4 @@
   114.4 -(*  Title:      HOLCF/Tools/repdef.ML
   114.5 +(*  Title:      HOL/HOLCF/Tools/domaindef.ML
   114.6      Author:     Brian Huffman
   114.7  
   114.8  Defining representable domains using algebraic deflations.
   115.1 --- a/src/HOL/HOLCF/Tools/fixrec.ML	Tue Mar 29 17:30:26 2011 +0200
   115.2 +++ b/src/HOL/HOLCF/Tools/fixrec.ML	Tue Mar 29 17:47:11 2011 +0200
   115.3 @@ -1,4 +1,4 @@
   115.4 -(*  Title:      HOLCF/Tools/fixrec.ML
   115.5 +(*  Title:      HOL/HOLCF/Tools/fixrec.ML
   115.6      Author:     Amber Telfer and Brian Huffman
   115.7  
   115.8  Recursive function definition package for HOLCF.
   116.1 --- a/src/HOL/HOLCF/Tools/holcf_library.ML	Tue Mar 29 17:30:26 2011 +0200
   116.2 +++ b/src/HOL/HOLCF/Tools/holcf_library.ML	Tue Mar 29 17:47:11 2011 +0200
   116.3 @@ -1,4 +1,4 @@
   116.4 -(*  Title:      HOLCF/Tools/holcf_library.ML
   116.5 +(*  Title:      HOL/HOLCF/Tools/holcf_library.ML
   116.6      Author:     Brian Huffman
   116.7  
   116.8  Functions for constructing HOLCF types and terms.
   117.1 --- a/src/HOL/HOLCF/Tr.thy	Tue Mar 29 17:30:26 2011 +0200
   117.2 +++ b/src/HOL/HOLCF/Tr.thy	Tue Mar 29 17:47:11 2011 +0200
   117.3 @@ -1,4 +1,4 @@
   117.4 -(*  Title:      HOLCF/Tr.thy
   117.5 +(*  Title:      HOL/HOLCF/Tr.thy
   117.6      Author:     Franz Regensburger
   117.7  *)
   117.8  
   118.1 --- a/src/HOL/HOLCF/Tutorial/Domain_ex.thy	Tue Mar 29 17:30:26 2011 +0200
   118.2 +++ b/src/HOL/HOLCF/Tutorial/Domain_ex.thy	Tue Mar 29 17:47:11 2011 +0200
   118.3 @@ -1,4 +1,4 @@
   118.4 -(*  Title:      HOLCF/ex/Domain_ex.thy
   118.5 +(*  Title:      HOL/HOLCF/Tutorial/Domain_ex.thy
   118.6      Author:     Brian Huffman
   118.7  *)
   118.8  
   119.1 --- a/src/HOL/HOLCF/Tutorial/Fixrec_ex.thy	Tue Mar 29 17:30:26 2011 +0200
   119.2 +++ b/src/HOL/HOLCF/Tutorial/Fixrec_ex.thy	Tue Mar 29 17:47:11 2011 +0200
   119.3 @@ -1,4 +1,4 @@
   119.4 -(*  Title:      HOLCF/ex/Fixrec_ex.thy
   119.5 +(*  Title:      HOL/HOLCF/Tutorial/Fixrec_ex.thy
   119.6      Author:     Brian Huffman
   119.7  *)
   119.8  
   120.1 --- a/src/HOL/HOLCF/Tutorial/New_Domain.thy	Tue Mar 29 17:30:26 2011 +0200
   120.2 +++ b/src/HOL/HOLCF/Tutorial/New_Domain.thy	Tue Mar 29 17:47:11 2011 +0200
   120.3 @@ -1,4 +1,4 @@
   120.4 -(*  Title:      HOLCF/ex/New_Domain.thy
   120.5 +(*  Title:      HOL/HOLCF/Tutorial/New_Domain.thy
   120.6      Author:     Brian Huffman
   120.7  *)
   120.8  
   121.1 --- a/src/HOL/HOLCF/Universal.thy	Tue Mar 29 17:30:26 2011 +0200
   121.2 +++ b/src/HOL/HOLCF/Universal.thy	Tue Mar 29 17:47:11 2011 +0200
   121.3 @@ -1,4 +1,4 @@
   121.4 -(*  Title:      HOLCF/Universal.thy
   121.5 +(*  Title:      HOL/HOLCF/Universal.thy
   121.6      Author:     Brian Huffman
   121.7  *)
   121.8  
   122.1 --- a/src/HOL/HOLCF/Up.thy	Tue Mar 29 17:30:26 2011 +0200
   122.2 +++ b/src/HOL/HOLCF/Up.thy	Tue Mar 29 17:47:11 2011 +0200
   122.3 @@ -1,4 +1,4 @@
   122.4 -(*  Title:      HOLCF/Up.thy
   122.5 +(*  Title:      HOL/HOLCF/Up.thy
   122.6      Author:     Franz Regensburger
   122.7      Author:     Brian Huffman
   122.8  *)
   123.1 --- a/src/HOL/HOLCF/UpperPD.thy	Tue Mar 29 17:30:26 2011 +0200
   123.2 +++ b/src/HOL/HOLCF/UpperPD.thy	Tue Mar 29 17:47:11 2011 +0200
   123.3 @@ -1,4 +1,4 @@
   123.4 -(*  Title:      HOLCF/UpperPD.thy
   123.5 +(*  Title:      HOL/HOLCF/UpperPD.thy
   123.6      Author:     Brian Huffman
   123.7  *)
   123.8  
   124.1 --- a/src/HOL/HOLCF/ex/Dnat.thy	Tue Mar 29 17:30:26 2011 +0200
   124.2 +++ b/src/HOL/HOLCF/ex/Dnat.thy	Tue Mar 29 17:47:11 2011 +0200
   124.3 @@ -1,4 +1,4 @@
   124.4 -(*  Title:      HOLCF/Dnat.thy
   124.5 +(*  Title:      HOL/HOLCF/ex/Dnat.thy
   124.6      Author:     Franz Regensburger
   124.7  
   124.8  Theory for the domain of natural numbers  dnat = one ++ dnat
   125.1 --- a/src/HOL/HOLCF/ex/Domain_Proofs.thy	Tue Mar 29 17:30:26 2011 +0200
   125.2 +++ b/src/HOL/HOLCF/ex/Domain_Proofs.thy	Tue Mar 29 17:47:11 2011 +0200
   125.3 @@ -1,4 +1,4 @@
   125.4 -(*  Title:      HOLCF/ex/Domain_Proofs.thy
   125.5 +(*  Title:      HOL/HOLCF/ex/Domain_Proofs.thy
   125.6      Author:     Brian Huffman
   125.7  *)
   125.8  
   126.1 --- a/src/HOL/HOLCF/ex/Fix2.thy	Tue Mar 29 17:30:26 2011 +0200
   126.2 +++ b/src/HOL/HOLCF/ex/Fix2.thy	Tue Mar 29 17:47:11 2011 +0200
   126.3 @@ -1,4 +1,4 @@
   126.4 -(*  Title:      HOLCF/ex/Fix2.thy
   126.5 +(*  Title:      HOL/HOLCF/ex/Fix2.thy
   126.6      Author:     Franz Regensburger
   126.7  
   126.8  Show that fix is the unique least fixed-point operator.
   127.1 --- a/src/HOL/HOLCF/ex/Hoare.thy	Tue Mar 29 17:30:26 2011 +0200
   127.2 +++ b/src/HOL/HOLCF/ex/Hoare.thy	Tue Mar 29 17:47:11 2011 +0200
   127.3 @@ -1,4 +1,4 @@
   127.4 -(*  Title:      HOLCF/ex/hoare.thy
   127.5 +(*  Title:      HOL/HOLCF/ex/Hoare.thy
   127.6      Author:     Franz Regensburger
   127.7  
   127.8  Theory for an example by C.A.R. Hoare
   128.1 --- a/src/HOL/HOLCF/ex/Letrec.thy	Tue Mar 29 17:30:26 2011 +0200
   128.2 +++ b/src/HOL/HOLCF/ex/Letrec.thy	Tue Mar 29 17:47:11 2011 +0200
   128.3 @@ -1,4 +1,4 @@
   128.4 -(*  Title:      HOLCF/ex/Letrec.thy
   128.5 +(*  Title:      HOL/HOLCF/ex/Letrec.thy
   128.6      Author:     Brian Huffman
   128.7  *)
   128.8  
   129.1 --- a/src/HOL/HOLCF/ex/Loop.thy	Tue Mar 29 17:30:26 2011 +0200
   129.2 +++ b/src/HOL/HOLCF/ex/Loop.thy	Tue Mar 29 17:47:11 2011 +0200
   129.3 @@ -1,4 +1,4 @@
   129.4 -(*  Title:      HOLCF/ex/Loop.thy
   129.5 +(*  Title:      HOL/HOLCF/ex/Loop.thy
   129.6      Author:     Franz Regensburger
   129.7  *)
   129.8  
   130.1 --- a/src/HOL/HOLCF/ex/Pattern_Match.thy	Tue Mar 29 17:30:26 2011 +0200
   130.2 +++ b/src/HOL/HOLCF/ex/Pattern_Match.thy	Tue Mar 29 17:47:11 2011 +0200
   130.3 @@ -1,4 +1,4 @@
   130.4 -(*  Title:      HOLCF/ex/Pattern_Match.thy
   130.5 +(*  Title:      HOL/HOLCF/ex/Pattern_Match.thy
   130.6      Author:     Brian Huffman
   130.7  *)
   130.8  
   131.1 --- a/src/HOL/HOLCF/ex/Powerdomain_ex.thy	Tue Mar 29 17:30:26 2011 +0200
   131.2 +++ b/src/HOL/HOLCF/ex/Powerdomain_ex.thy	Tue Mar 29 17:47:11 2011 +0200
   131.3 @@ -1,4 +1,4 @@
   131.4 -(*  Title:      HOLCF/ex/Powerdomain_ex.thy
   131.5 +(*  Title:      HOL/HOLCF/ex/Powerdomain_ex.thy
   131.6      Author:     Brian Huffman
   131.7  *)
   131.8  
   132.1 --- a/src/HOL/HOLCF/ex/ROOT.ML	Tue Mar 29 17:30:26 2011 +0200
   132.2 +++ b/src/HOL/HOLCF/ex/ROOT.ML	Tue Mar 29 17:47:11 2011 +0200
   132.3 @@ -1,4 +1,4 @@
   132.4 -(*  Title:      HOLCF/ex/ROOT.ML
   132.5 +(*  Title:      HOL/HOLCF/ex/ROOT.ML
   132.6  
   132.7  Misc HOLCF examples.
   132.8  *)