--- a/src/Doc/Functions/Functions.thy Fri Dec 14 16:24:12 2012 +0100
+++ b/src/Doc/Functions/Functions.thy Fri Dec 14 16:33:22 2012 +0100
@@ -1,4 +1,4 @@
-(* Title: Doc/Functions/Fundefs.thy
+(* Title: Doc/Functions/Functions.thy
Author: Alexander Krauss, TU Muenchen
Tutorial for function definitions with the new "function" package.
--- a/src/Doc/Tutorial/Protocol/Public.thy Fri Dec 14 16:24:12 2012 +0100
+++ b/src/Doc/Tutorial/Protocol/Public.thy Fri Dec 14 16:33:22 2012 +0100
@@ -1,4 +1,4 @@
-(* Title: HOL/Auth/Public
+(* Title: Doc/Tutorial/Protocol/Public.thy
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1996 University of Cambridge
--- a/src/Doc/ZF/If.thy Fri Dec 14 16:24:12 2012 +0100
+++ b/src/Doc/ZF/If.thy Fri Dec 14 16:33:22 2012 +0100
@@ -1,4 +1,4 @@
-(* Title: FOL/ex/If.ML
+(* Title: Doc/ZF/If.thy
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
--- a/src/HOL/BNF/Examples/Derivation_Trees/DTree.thy Fri Dec 14 16:24:12 2012 +0100
+++ b/src/HOL/BNF/Examples/Derivation_Trees/DTree.thy Fri Dec 14 16:33:22 2012 +0100
@@ -1,4 +1,4 @@
-(* Title: HOL/BNF/Examples/Infinite_Derivation_Trees/DTree.thy
+(* Title: HOL/BNF/Examples/Derivation_Trees/DTree.thy
Author: Andrei Popescu, TU Muenchen
Copyright 2012
--- a/src/HOL/BNF/Examples/Koenig.thy Fri Dec 14 16:24:12 2012 +0100
+++ b/src/HOL/BNF/Examples/Koenig.thy Fri Dec 14 16:33:22 2012 +0100
@@ -1,4 +1,4 @@
-(* Title: HOL/BNF/Examples/Stream.thy
+(* Title: HOL/BNF/Examples/Koenig.thy
Author: Dmitriy Traytel, TU Muenchen
Author: Andrei Popescu, TU Muenchen
Copyright 2012
--- a/src/HOL/Library/Refute.thy Fri Dec 14 16:24:12 2012 +0100
+++ b/src/HOL/Library/Refute.thy Fri Dec 14 16:33:22 2012 +0100
@@ -1,4 +1,4 @@
-(* Title: HOL/Refute.thy
+(* Title: HOL/Library/Refute.thy
Author: Tjark Weber
Copyright 2003-2007
--- a/src/HOL/Library/refute.ML Fri Dec 14 16:24:12 2012 +0100
+++ b/src/HOL/Library/refute.ML Fri Dec 14 16:33:22 2012 +0100
@@ -1,4 +1,4 @@
-(* Title: HOL/Tools/refute.ML
+(* Title: HOL/Library/refute.ML
Author: Tjark Weber, TU Muenchen
Finite model generation for HOL formulas, using a SAT solver.
--- a/src/HOL/Probability/Measurable.thy Fri Dec 14 16:24:12 2012 +0100
+++ b/src/HOL/Probability/Measurable.thy Fri Dec 14 16:33:22 2012 +0100
@@ -1,4 +1,4 @@
-(* Title: HOL/Probability/measurable.ML
+(* Title: HOL/Probability/Measurable.thy
Author: Johannes Hölzl <hoelzl@in.tum.de>
*)
theory Measurable
--- a/src/HOL/Probability/Regularity.thy Fri Dec 14 16:24:12 2012 +0100
+++ b/src/HOL/Probability/Regularity.thy Fri Dec 14 16:33:22 2012 +0100
@@ -1,4 +1,4 @@
-(* Title: HOL/Probability/Projective_Family.thy
+(* Title: HOL/Probability/Regularity.thy
Author: Fabian Immler, TU München
*)