1.1 --- a/src/Doc/Functions/Functions.thy	Fri Dec 14 16:24:12 2012 +0100
     1.2 +++ b/src/Doc/Functions/Functions.thy	Fri Dec 14 16:33:22 2012 +0100
     1.3 @@ -1,4 +1,4 @@
     1.4 -(*  Title:      Doc/Functions/Fundefs.thy
     1.5 +(*  Title:      Doc/Functions/Functions.thy
     1.6      Author:     Alexander Krauss, TU Muenchen
     1.7  
     1.8  Tutorial for function definitions with the new "function" package.

     2.1 --- a/src/Doc/Tutorial/Protocol/Public.thy	Fri Dec 14 16:24:12 2012 +0100
     2.2 +++ b/src/Doc/Tutorial/Protocol/Public.thy	Fri Dec 14 16:33:22 2012 +0100
     2.3 @@ -1,4 +1,4 @@
     2.4 -(*  Title:      HOL/Auth/Public
     2.5 +(*  Title:      Doc/Tutorial/Protocol/Public.thy
     2.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2.7      Copyright   1996  University of Cambridge
     2.8  

     3.1 --- a/src/Doc/ZF/If.thy	Fri Dec 14 16:24:12 2012 +0100
     3.2 +++ b/src/Doc/ZF/If.thy	Fri Dec 14 16:33:22 2012 +0100
     3.3 @@ -1,4 +1,4 @@
     3.4 -(*  Title:      FOL/ex/If.ML
     3.5 +(*  Title:      Doc/ZF/If.thy
     3.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3.7      Copyright   1991  University of Cambridge
     3.8  

     4.1 --- a/src/HOL/BNF/Examples/Derivation_Trees/DTree.thy	Fri Dec 14 16:24:12 2012 +0100
     4.2 +++ b/src/HOL/BNF/Examples/Derivation_Trees/DTree.thy	Fri Dec 14 16:33:22 2012 +0100
     4.3 @@ -1,4 +1,4 @@
     4.4 -(*  Title:      HOL/BNF/Examples/Infinite_Derivation_Trees/DTree.thy
     4.5 +(*  Title:      HOL/BNF/Examples/Derivation_Trees/DTree.thy
     4.6      Author:     Andrei Popescu, TU Muenchen
     4.7      Copyright   2012
     4.8  

     5.1 --- a/src/HOL/BNF/Examples/Koenig.thy	Fri Dec 14 16:24:12 2012 +0100
     5.2 +++ b/src/HOL/BNF/Examples/Koenig.thy	Fri Dec 14 16:33:22 2012 +0100
     5.3 @@ -1,4 +1,4 @@
     5.4 -(*  Title:      HOL/BNF/Examples/Stream.thy
     5.5 +(*  Title:      HOL/BNF/Examples/Koenig.thy
     5.6      Author:     Dmitriy Traytel, TU Muenchen
     5.7      Author:     Andrei Popescu, TU Muenchen
     5.8      Copyright   2012

     6.1 --- a/src/HOL/Library/Refute.thy	Fri Dec 14 16:24:12 2012 +0100
     6.2 +++ b/src/HOL/Library/Refute.thy	Fri Dec 14 16:33:22 2012 +0100
     6.3 @@ -1,4 +1,4 @@
     6.4 -(*  Title:      HOL/Refute.thy
     6.5 +(*  Title:      HOL/Library/Refute.thy
     6.6      Author:     Tjark Weber
     6.7      Copyright   2003-2007
     6.8  

     7.1 --- a/src/HOL/Library/refute.ML	Fri Dec 14 16:24:12 2012 +0100
     7.2 +++ b/src/HOL/Library/refute.ML	Fri Dec 14 16:33:22 2012 +0100
     7.3 @@ -1,4 +1,4 @@
     7.4 -(*  Title:      HOL/Tools/refute.ML
     7.5 +(*  Title:      HOL/Library/refute.ML
     7.6      Author:     Tjark Weber, TU Muenchen
     7.7  
     7.8  Finite model generation for HOL formulas, using a SAT solver.

     8.1 --- a/src/HOL/Probability/Measurable.thy	Fri Dec 14 16:24:12 2012 +0100
     8.2 +++ b/src/HOL/Probability/Measurable.thy	Fri Dec 14 16:33:22 2012 +0100
     8.3 @@ -1,4 +1,4 @@
     8.4 -(*  Title:      HOL/Probability/measurable.ML
     8.5 +(*  Title:      HOL/Probability/Measurable.thy
     8.6      Author:     Johannes Hölzl <hoelzl@in.tum.de>
     8.7  *)
     8.8  theory Measurable

     9.1 --- a/src/HOL/Probability/Regularity.thy	Fri Dec 14 16:24:12 2012 +0100
     9.2 +++ b/src/HOL/Probability/Regularity.thy	Fri Dec 14 16:33:22 2012 +0100
     9.3 @@ -1,4 +1,4 @@
     9.4 -(*  Title:      HOL/Probability/Projective_Family.thy
     9.5 +(*  Title:      HOL/Probability/Regularity.thy
     9.6      Author:     Fabian Immler, TU München
     9.7  *)
     9.8