# HG changeset patch
# User wenzelm
# Date 1475410063 -7200
# Node ID 3aa9837d05c7ec978946fa54c23604cd99b3c784
# Parent  0d8cd1f3c26db5d0c7dae2460847cff470aa0513
updated headers;

diff -r 0d8cd1f3c26d -r 3aa9837d05c7 src/HOL/Analysis/Continuous_Extension.thy
--- 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
 *)
 
diff -r 0d8cd1f3c26d -r 3aa9837d05c7 src/HOL/Analysis/Gamma_Function.thy
--- 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
 *)
 
diff -r 0d8cd1f3c26d -r 3aa9837d05c7 src/HOL/Analysis/Summation_Tests.thy
--- 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
 *)
 
diff -r 0d8cd1f3c26d -r 3aa9837d05c7 src/HOL/Library/Predicate_Compile_Quickcheck.thy
--- 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
 *)
 
diff -r 0d8cd1f3c26d -r 3aa9837d05c7 src/HOL/Probability/Characteristic_Functions.thy
--- 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)
 *)
 
diff -r 0d8cd1f3c26d -r 3aa9837d05c7 src/HOL/Probability/Distribution_Functions.thy
--- 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)
 *)
 
diff -r 0d8cd1f3c26d -r 3aa9837d05c7 src/HOL/Tools/Argo/argo_real.ML
--- 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.
diff -r 0d8cd1f3c26d -r 3aa9837d05c7 src/HOL/Tools/Argo/argo_sat_solver.ML
--- 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.
diff -r 0d8cd1f3c26d -r 3aa9837d05c7 src/HOL/Tools/Argo/argo_tactic.ML
--- 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.
diff -r 0d8cd1f3c26d -r 3aa9837d05c7 src/Pure/General/json.scala
--- 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.
diff -r 0d8cd1f3c26d -r 3aa9837d05c7 src/Pure/Tools/ci_api.scala
--- 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.
diff -r 0d8cd1f3c26d -r 3aa9837d05c7 src/Tools/Argo/argo_expr.ML
--- 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.
diff -r 0d8cd1f3c26d -r 3aa9837d05c7 src/Tools/Argo/argo_thy.ML
--- 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.