updated headers;
authorwenzelm
Fri, 22 Feb 2013 14:39:12 +0100
changeset 52377a7a04b449e8b
parent 52376 67cc209493b2
child 52378 83252b0605be
updated headers;
src/HOL/ex/Reflection_Examples.thy
src/Pure/Tools/ml_statistics.scala
src/Pure/Tools/task_statistics.scala
src/Tools/jEdit/src/fold_handling.scala
     1.1 --- a/src/HOL/ex/Reflection_Examples.thy	Fri Feb 22 14:38:52 2013 +0100
     1.2 +++ b/src/HOL/ex/Reflection_Examples.thy	Fri Feb 22 14:39:12 2013 +0100
     1.3 @@ -1,4 +1,4 @@
     1.4 -(*  Title:      HOL/ex/Reflection_Ex.thy
     1.5 +(*  Title:      HOL/ex/Reflection_Examples.thy
     1.6      Author:     Amine Chaieb, TU Muenchen
     1.7  *)
     1.8  
     2.1 --- a/src/Pure/Tools/ml_statistics.scala	Fri Feb 22 14:38:52 2013 +0100
     2.2 +++ b/src/Pure/Tools/ml_statistics.scala	Fri Feb 22 14:39:12 2013 +0100
     2.3 @@ -1,4 +1,4 @@
     2.4 -/*  Title:      Pure/ML/ml_statistics.ML
     2.5 +/*  Title:      Pure/Tools/ml_statistics.scala
     2.6      Author:     Makarius
     2.7  
     2.8  ML runtime statistics.
     3.1 --- a/src/Pure/Tools/task_statistics.scala	Fri Feb 22 14:38:52 2013 +0100
     3.2 +++ b/src/Pure/Tools/task_statistics.scala	Fri Feb 22 14:39:12 2013 +0100
     3.3 @@ -1,4 +1,4 @@
     3.4 -/*  Title:      Pure/ML/task_statistics.ML
     3.5 +/*  Title:      Pure/Tools/task_statistics.scala
     3.6      Author:     Makarius
     3.7  
     3.8  Future task runtime statistics.
     4.1 --- a/src/Tools/jEdit/src/fold_handling.scala	Fri Feb 22 14:38:52 2013 +0100
     4.2 +++ b/src/Tools/jEdit/src/fold_handling.scala	Fri Feb 22 14:39:12 2013 +0100
     4.3 @@ -1,4 +1,4 @@
     4.4 -/*  Title:      Tools/jEdit/src/fold_handler.scala
     4.5 +/*  Title:      Tools/jEdit/src/fold_handling.scala
     4.6      Author:     Makarius
     4.7  
     4.8  Handling of folds within the text structure.