# HG changeset patch
# User wenzelm
# Date 1451998131 -3600
# Node ID 1cfd5d6049372e63ee101d8bd4300289349fbc54
# Parent  af58628952f0589e85330ddaf5a82e36d54debd8
updated headers;

diff -r af58628952f0 -r 1cfd5d604937 src/HOL/Imperative_HOL/ex/List_Sublist.thy
--- a/src/HOL/Imperative_HOL/ex/List_Sublist.thy	Tue Jan 05 13:41:29 2016 +0100
+++ b/src/HOL/Imperative_HOL/ex/List_Sublist.thy	Tue Jan 05 13:48:51 2016 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Imperative_HOL/ex/Sublist.thy
+(*  Title:      HOL/Imperative_HOL/ex/List_Sublist.thy
     Author:     Lukas Bulwahn, TU Muenchen
 *)
 
diff -r af58628952f0 -r 1cfd5d604937 src/HOL/Library/Bourbaki_Witt_Fixpoint.thy
--- a/src/HOL/Library/Bourbaki_Witt_Fixpoint.thy	Tue Jan 05 13:41:29 2016 +0100
+++ b/src/HOL/Library/Bourbaki_Witt_Fixpoint.thy	Tue Jan 05 13:48:51 2016 +0100
@@ -1,5 +1,6 @@
-(* Title: Bourbaki_Witt_Fixpoint.thy
-   Author: Andreas Lochbihler, ETH Zurich *)
+(*  Title:      HOL/Library/Bourbaki_Witt_Fixpoint.thy
+    Author:     Andreas Lochbihler, ETH Zurich
+*)
 
 section \<open>The Bourbaki-Witt tower construction for transfinite iteration\<close>
 
diff -r af58628952f0 -r 1cfd5d604937 src/HOL/Library/Quadratic_Discriminant.thy
--- a/src/HOL/Library/Quadratic_Discriminant.thy	Tue Jan 05 13:41:29 2016 +0100
+++ b/src/HOL/Library/Quadratic_Discriminant.thy	Tue Jan 05 13:48:51 2016 +0100
@@ -1,4 +1,4 @@
-(*  Title:       Roots of real quadratics
+(*  Title:       HOL/Library/Quadratic_Discriminant.thy
     Author:      Tim Makarios <tjm1983 at gmail.com>, 2012
 
 Originally from the AFP entry Tarskis_Geometry
diff -r af58628952f0 -r 1cfd5d604937 src/HOL/Library/old_recdef.ML
--- a/src/HOL/Library/old_recdef.ML	Tue Jan 05 13:41:29 2016 +0100
+++ b/src/HOL/Library/old_recdef.ML	Tue Jan 05 13:48:51 2016 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Tools/old_recdef.ML
+(*  Title:      HOL/Library/old_recdef.ML
     Author:     Konrad Slind, Cambridge University Computer Laboratory
     Author:     Lucas Dixon, University of Edinburgh
 
diff -r af58628952f0 -r 1cfd5d604937 src/HOL/Tools/boolean_algebra_cancel.ML
--- a/src/HOL/Tools/boolean_algebra_cancel.ML	Tue Jan 05 13:41:29 2016 +0100
+++ b/src/HOL/Tools/boolean_algebra_cancel.ML	Tue Jan 05 13:48:51 2016 +0100
@@ -1,4 +1,4 @@
-(*  Title:      boolean_algebra_cancel.ML
+(*  Title:      HOL/Tools/boolean_algebra_cancel.ML
     Author:     Andreas Lochbihler, ETH Zurich
 
 Simplification procedures for boolean algebras:
diff -r af58628952f0 -r 1cfd5d604937 src/Pure/RAW/ml_compiler_parameters.ML
--- a/src/Pure/RAW/ml_compiler_parameters.ML	Tue Jan 05 13:41:29 2016 +0100
+++ b/src/Pure/RAW/ml_compiler_parameters.ML	Tue Jan 05 13:48:51 2016 +0100
@@ -1,4 +1,4 @@
-(*  Title:      Pure/ML/ml_compiler_parameters.ML
+(*  Title:      Pure/RAW/ml_compiler_parameters.ML
     Author:     Makarius
 
 Additional ML compiler parameters for Poly/ML.
diff -r af58628952f0 -r 1cfd5d604937 src/Pure/RAW/ml_compiler_parameters_polyml-5.6.ML
--- a/src/Pure/RAW/ml_compiler_parameters_polyml-5.6.ML	Tue Jan 05 13:41:29 2016 +0100
+++ b/src/Pure/RAW/ml_compiler_parameters_polyml-5.6.ML	Tue Jan 05 13:48:51 2016 +0100
@@ -1,4 +1,4 @@
-(*  Title:      Pure/ML/ml_compiler_parameters_polyml-5.6.ML
+(*  Title:      Pure/RAW/ml_compiler_parameters_polyml-5.6.ML
     Author:     Makarius
 
 Additional ML compiler parameters for Poly/ML 5.6, or later.
diff -r af58628952f0 -r 1cfd5d604937 src/Pure/RAW/ml_debugger.ML
--- a/src/Pure/RAW/ml_debugger.ML	Tue Jan 05 13:41:29 2016 +0100
+++ b/src/Pure/RAW/ml_debugger.ML	Tue Jan 05 13:48:51 2016 +0100
@@ -1,4 +1,4 @@
-(*  Title:      Pure/ML/ml_debugger.ML
+(*  Title:      Pure/RAW/ml_debugger.ML
     Author:     Makarius
 
 ML debugger interface -- dummy version.
diff -r af58628952f0 -r 1cfd5d604937 src/Pure/RAW/ml_parse_tree.ML
--- a/src/Pure/RAW/ml_parse_tree.ML	Tue Jan 05 13:41:29 2016 +0100
+++ b/src/Pure/RAW/ml_parse_tree.ML	Tue Jan 05 13:48:51 2016 +0100
@@ -1,4 +1,4 @@
-(*  Title:      Pure/ML/ml_parse_tree.ML
+(*  Title:      Pure/RAW/ml_parse_tree.ML
     Author:     Makarius
 
 Additional ML parse tree components for Poly/ML.
diff -r af58628952f0 -r 1cfd5d604937 src/Pure/System/cygwin.scala
--- a/src/Pure/System/cygwin.scala	Tue Jan 05 13:41:29 2016 +0100
+++ b/src/Pure/System/cygwin.scala	Tue Jan 05 13:48:51 2016 +0100
@@ -1,4 +1,4 @@
-/*  Title:      Pure/Tools/cygwin.scala
+/*  Title:      Pure/System/cygwin.scala
     Author:     Makarius
 
 Cygwin as POSIX emulation on Windows.
diff -r af58628952f0 -r 1cfd5d604937 src/Pure/Thy/document_antiquotations.ML
--- a/src/Pure/Thy/document_antiquotations.ML	Tue Jan 05 13:41:29 2016 +0100
+++ b/src/Pure/Thy/document_antiquotations.ML	Tue Jan 05 13:48:51 2016 +0100
@@ -1,4 +1,4 @@
-(*  Title:      Pure/ML/document_antiquotations.ML
+(*  Title:      Pure/Thy/document_antiquotations.ML
     Author:     Makarius
 
 Miscellaneous document antiquotations.