# HG changeset patch
# User wenzelm
# Date 1355499202 -3600
# Node ID 6266e44b3396407adde2d79ddd351118cb760d4a
# Parent  b2aa899b3f2d7138d5f31ab7ca316866c2cf631a
updated some headers;

diff -r b2aa899b3f2d -r 6266e44b3396 src/Doc/Functions/Functions.thy
--- 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.
diff -r b2aa899b3f2d -r 6266e44b3396 src/Doc/Tutorial/Protocol/Public.thy
--- 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
 
diff -r b2aa899b3f2d -r 6266e44b3396 src/Doc/ZF/If.thy
--- 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
 
diff -r b2aa899b3f2d -r 6266e44b3396 src/HOL/BNF/Examples/Derivation_Trees/DTree.thy
--- 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
 
diff -r b2aa899b3f2d -r 6266e44b3396 src/HOL/BNF/Examples/Koenig.thy
--- 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
diff -r b2aa899b3f2d -r 6266e44b3396 src/HOL/Library/Refute.thy
--- 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
 
diff -r b2aa899b3f2d -r 6266e44b3396 src/HOL/Library/refute.ML
--- 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.
diff -r b2aa899b3f2d -r 6266e44b3396 src/HOL/Probability/Measurable.thy
--- 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
diff -r b2aa899b3f2d -r 6266e44b3396 src/HOL/Probability/Regularity.thy
--- 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
 *)