updated some headers;
authorwenzelm
Fri, 14 Dec 2012 16:33:22 +0100
changeset 50530 6266e44b3396
parent 50529 b2aa899b3f2d
child 50531 f841ac0cb757
updated some headers;
src/Doc/Functions/Functions.thy
src/Doc/Tutorial/Protocol/Public.thy
src/Doc/ZF/If.thy
src/HOL/BNF/Examples/Derivation_Trees/DTree.thy
src/HOL/BNF/Examples/Koenig.thy
src/HOL/Library/Refute.thy
src/HOL/Library/refute.ML
src/HOL/Probability/Measurable.thy
src/HOL/Probability/Regularity.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.
--- 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
 *)