--- a/src/HOL/Analysis/Continuous_Extension.thy Sun Oct 02 13:47:39 2016 +0200
+++ b/src/HOL/Analysis/Continuous_Extension.thy Sun Oct 02 14:07:43 2016 +0200
@@ -1,4 +1,4 @@
-(* Title: HOL/Analysis/Extension.thy
+(* Title: HOL/Analysis/Continuous_Extension.thy
Authors: LC Paulson, based on material from HOL Light
*)
--- a/src/HOL/Analysis/Gamma_Function.thy Sun Oct 02 13:47:39 2016 +0200
+++ b/src/HOL/Analysis/Gamma_Function.thy Sun Oct 02 14:07:43 2016 +0200
@@ -1,4 +1,4 @@
-(* Title: HOL/Analysis/Gamma.thy
+(* Title: HOL/Analysis/Gamma_Function.thy
Author: Manuel Eberl, TU München
*)
--- a/src/HOL/Analysis/Summation_Tests.thy Sun Oct 02 13:47:39 2016 +0200
+++ b/src/HOL/Analysis/Summation_Tests.thy Sun Oct 02 14:07:43 2016 +0200
@@ -1,4 +1,4 @@
-(* Title: HOL/Analysis/Summation.thy
+(* Title: HOL/Analysis/Summation_Tests.thy
Author: Manuel Eberl, TU München
*)
--- a/src/HOL/Library/Predicate_Compile_Quickcheck.thy Sun Oct 02 13:47:39 2016 +0200
+++ b/src/HOL/Library/Predicate_Compile_Quickcheck.thy Sun Oct 02 14:07:43 2016 +0200
@@ -1,4 +1,4 @@
-(* Title: HOL/Library/Predicate_Compile_Alternative_Defs.thy
+(* Title: HOL/Library/Predicate_Compile_Quickcheck.thy
Author: Lukas Bulwahn, TU Muenchen
*)
--- a/src/HOL/Probability/Characteristic_Functions.thy Sun Oct 02 13:47:39 2016 +0200
+++ b/src/HOL/Probability/Characteristic_Functions.thy Sun Oct 02 14:07:43 2016 +0200
@@ -1,4 +1,4 @@
-(* Title: Characteristic_Functions.thy
+(* Title: HOL/Probability/Characteristic_Functions.thy
Authors: Jeremy Avigad (CMU), Luke Serafin (CMU), Johannes Hölzl (TUM)
*)
--- a/src/HOL/Probability/Distribution_Functions.thy Sun Oct 02 13:47:39 2016 +0200
+++ b/src/HOL/Probability/Distribution_Functions.thy Sun Oct 02 14:07:43 2016 +0200
@@ -1,4 +1,4 @@
-(* Title: Distribution_Functions.thy
+(* Title: HOL/Probability/Distribution_Functions.thy
Authors: Jeremy Avigad (CMU) and Luke Serafin (CMU)
*)
--- a/src/HOL/Tools/Argo/argo_real.ML Sun Oct 02 13:47:39 2016 +0200
+++ b/src/HOL/Tools/Argo/argo_real.ML Sun Oct 02 14:07:43 2016 +0200
@@ -1,4 +1,4 @@
-(* Title: HOL/Tools/argo_real.ML
+(* Title: HOL/Tools/Argo/argo_real.ML
Author: Sascha Boehme
Extension of the Argo tactic for the reals.
--- a/src/HOL/Tools/Argo/argo_sat_solver.ML Sun Oct 02 13:47:39 2016 +0200
+++ b/src/HOL/Tools/Argo/argo_sat_solver.ML Sun Oct 02 14:07:43 2016 +0200
@@ -1,4 +1,4 @@
-(* Title: HOL/Tools/argo_sat_solver.ML
+(* Title: HOL/Tools/Argo/argo_sat_solver.ML
Author: Sascha Boehme
A SAT solver based on the Argo solver.
--- a/src/HOL/Tools/Argo/argo_tactic.ML Sun Oct 02 13:47:39 2016 +0200
+++ b/src/HOL/Tools/Argo/argo_tactic.ML Sun Oct 02 14:07:43 2016 +0200
@@ -1,4 +1,4 @@
-(* Title: HOL/Tools/argo_tactic.ML
+(* Title: HOL/Tools/Argo/argo_tactic.ML
Author: Sascha Boehme
HOL method and tactic for the Argo solver.
--- a/src/Pure/General/json.scala Sun Oct 02 13:47:39 2016 +0200
+++ b/src/Pure/General/json.scala Sun Oct 02 14:07:43 2016 +0200
@@ -1,4 +1,4 @@
-/* Title: Pure/Tools/json.scala
+/* Title: Pure/General/json.scala
Author: Makarius
Support for JSON parsing.
--- a/src/Pure/Tools/ci_api.scala Sun Oct 02 13:47:39 2016 +0200
+++ b/src/Pure/Tools/ci_api.scala Sun Oct 02 14:07:43 2016 +0200
@@ -1,4 +1,4 @@
-/* Title: Pure/Tools/build.scala
+/* Title: Pure/Tools/ci_api.scala
Author: Makarius
API for Isabelle Jenkins continuous integration services.
--- a/src/Tools/Argo/argo_expr.ML Sun Oct 02 13:47:39 2016 +0200
+++ b/src/Tools/Argo/argo_expr.ML Sun Oct 02 14:07:43 2016 +0200
@@ -1,4 +1,4 @@
-(* Title: Tools/Argo/sid_expr.ML
+(* Title: Tools/Argo/argo_expr.ML
Author: Sascha Boehme
The input language of the Argo solver.
--- a/src/Tools/Argo/argo_thy.ML Sun Oct 02 13:47:39 2016 +0200
+++ b/src/Tools/Argo/argo_thy.ML Sun Oct 02 14:07:43 2016 +0200
@@ -1,4 +1,4 @@
-(* Title: Tools/Argo/argo_theory.ML
+(* Title: Tools/Argo/argo_thy.ML
Author: Sascha Boehme
Combination of all theory solvers.