updated headers;
authorwenzelm
Tue Jan 05 13:48:51 2016 +0100 (2016-01-05)
changeset 620581cfd5d604937
parent 62057 af58628952f0
child 62059 2da6f4945295
updated headers;
src/HOL/Imperative_HOL/ex/List_Sublist.thy
src/HOL/Library/Bourbaki_Witt_Fixpoint.thy
src/HOL/Library/Quadratic_Discriminant.thy
src/HOL/Library/old_recdef.ML
src/HOL/Tools/boolean_algebra_cancel.ML
src/Pure/RAW/ml_compiler_parameters.ML
src/Pure/RAW/ml_compiler_parameters_polyml-5.6.ML
src/Pure/RAW/ml_debugger.ML
src/Pure/RAW/ml_parse_tree.ML
src/Pure/System/cygwin.scala
src/Pure/Thy/document_antiquotations.ML
     1.1 --- a/src/HOL/Imperative_HOL/ex/List_Sublist.thy	Tue Jan 05 13:41:29 2016 +0100
     1.2 +++ b/src/HOL/Imperative_HOL/ex/List_Sublist.thy	Tue Jan 05 13:48:51 2016 +0100
     1.3 @@ -1,4 +1,4 @@
     1.4 -(*  Title:      HOL/Imperative_HOL/ex/Sublist.thy
     1.5 +(*  Title:      HOL/Imperative_HOL/ex/List_Sublist.thy
     1.6      Author:     Lukas Bulwahn, TU Muenchen
     1.7  *)
     1.8  
     2.1 --- a/src/HOL/Library/Bourbaki_Witt_Fixpoint.thy	Tue Jan 05 13:41:29 2016 +0100
     2.2 +++ b/src/HOL/Library/Bourbaki_Witt_Fixpoint.thy	Tue Jan 05 13:48:51 2016 +0100
     2.3 @@ -1,5 +1,6 @@
     2.4 -(* Title: Bourbaki_Witt_Fixpoint.thy
     2.5 -   Author: Andreas Lochbihler, ETH Zurich *)
     2.6 +(*  Title:      HOL/Library/Bourbaki_Witt_Fixpoint.thy
     2.7 +    Author:     Andreas Lochbihler, ETH Zurich
     2.8 +*)
     2.9  
    2.10  section \<open>The Bourbaki-Witt tower construction for transfinite iteration\<close>
    2.11  
     3.1 --- a/src/HOL/Library/Quadratic_Discriminant.thy	Tue Jan 05 13:41:29 2016 +0100
     3.2 +++ b/src/HOL/Library/Quadratic_Discriminant.thy	Tue Jan 05 13:48:51 2016 +0100
     3.3 @@ -1,4 +1,4 @@
     3.4 -(*  Title:       Roots of real quadratics
     3.5 +(*  Title:       HOL/Library/Quadratic_Discriminant.thy
     3.6      Author:      Tim Makarios <tjm1983 at gmail.com>, 2012
     3.7  
     3.8  Originally from the AFP entry Tarskis_Geometry
     4.1 --- a/src/HOL/Library/old_recdef.ML	Tue Jan 05 13:41:29 2016 +0100
     4.2 +++ b/src/HOL/Library/old_recdef.ML	Tue Jan 05 13:48:51 2016 +0100
     4.3 @@ -1,4 +1,4 @@
     4.4 -(*  Title:      HOL/Tools/old_recdef.ML
     4.5 +(*  Title:      HOL/Library/old_recdef.ML
     4.6      Author:     Konrad Slind, Cambridge University Computer Laboratory
     4.7      Author:     Lucas Dixon, University of Edinburgh
     4.8  
     5.1 --- a/src/HOL/Tools/boolean_algebra_cancel.ML	Tue Jan 05 13:41:29 2016 +0100
     5.2 +++ b/src/HOL/Tools/boolean_algebra_cancel.ML	Tue Jan 05 13:48:51 2016 +0100
     5.3 @@ -1,4 +1,4 @@
     5.4 -(*  Title:      boolean_algebra_cancel.ML
     5.5 +(*  Title:      HOL/Tools/boolean_algebra_cancel.ML
     5.6      Author:     Andreas Lochbihler, ETH Zurich
     5.7  
     5.8  Simplification procedures for boolean algebras:
     6.1 --- a/src/Pure/RAW/ml_compiler_parameters.ML	Tue Jan 05 13:41:29 2016 +0100
     6.2 +++ b/src/Pure/RAW/ml_compiler_parameters.ML	Tue Jan 05 13:48:51 2016 +0100
     6.3 @@ -1,4 +1,4 @@
     6.4 -(*  Title:      Pure/ML/ml_compiler_parameters.ML
     6.5 +(*  Title:      Pure/RAW/ml_compiler_parameters.ML
     6.6      Author:     Makarius
     6.7  
     6.8  Additional ML compiler parameters for Poly/ML.
     7.1 --- a/src/Pure/RAW/ml_compiler_parameters_polyml-5.6.ML	Tue Jan 05 13:41:29 2016 +0100
     7.2 +++ b/src/Pure/RAW/ml_compiler_parameters_polyml-5.6.ML	Tue Jan 05 13:48:51 2016 +0100
     7.3 @@ -1,4 +1,4 @@
     7.4 -(*  Title:      Pure/ML/ml_compiler_parameters_polyml-5.6.ML
     7.5 +(*  Title:      Pure/RAW/ml_compiler_parameters_polyml-5.6.ML
     7.6      Author:     Makarius
     7.7  
     7.8  Additional ML compiler parameters for Poly/ML 5.6, or later.
     8.1 --- a/src/Pure/RAW/ml_debugger.ML	Tue Jan 05 13:41:29 2016 +0100
     8.2 +++ b/src/Pure/RAW/ml_debugger.ML	Tue Jan 05 13:48:51 2016 +0100
     8.3 @@ -1,4 +1,4 @@
     8.4 -(*  Title:      Pure/ML/ml_debugger.ML
     8.5 +(*  Title:      Pure/RAW/ml_debugger.ML
     8.6      Author:     Makarius
     8.7  
     8.8  ML debugger interface -- dummy version.
     9.1 --- a/src/Pure/RAW/ml_parse_tree.ML	Tue Jan 05 13:41:29 2016 +0100
     9.2 +++ b/src/Pure/RAW/ml_parse_tree.ML	Tue Jan 05 13:48:51 2016 +0100
     9.3 @@ -1,4 +1,4 @@
     9.4 -(*  Title:      Pure/ML/ml_parse_tree.ML
     9.5 +(*  Title:      Pure/RAW/ml_parse_tree.ML
     9.6      Author:     Makarius
     9.7  
     9.8  Additional ML parse tree components for Poly/ML.
    10.1 --- a/src/Pure/System/cygwin.scala	Tue Jan 05 13:41:29 2016 +0100
    10.2 +++ b/src/Pure/System/cygwin.scala	Tue Jan 05 13:48:51 2016 +0100
    10.3 @@ -1,4 +1,4 @@
    10.4 -/*  Title:      Pure/Tools/cygwin.scala
    10.5 +/*  Title:      Pure/System/cygwin.scala
    10.6      Author:     Makarius
    10.7  
    10.8  Cygwin as POSIX emulation on Windows.
    11.1 --- a/src/Pure/Thy/document_antiquotations.ML	Tue Jan 05 13:41:29 2016 +0100
    11.2 +++ b/src/Pure/Thy/document_antiquotations.ML	Tue Jan 05 13:48:51 2016 +0100
    11.3 @@ -1,4 +1,4 @@
    11.4 -(*  Title:      Pure/ML/document_antiquotations.ML
    11.5 +(*  Title:      Pure/Thy/document_antiquotations.ML
    11.6      Author:     Makarius
    11.7  
    11.8  Miscellaneous document antiquotations.