updated headers;
authorwenzelm
Sun, 02 Oct 2016 14:07:43 +0200
changeset 63992 3aa9837d05c7
parent 63991 0d8cd1f3c26d
child 63993 9c0ff0c12116
updated headers;
src/HOL/Analysis/Continuous_Extension.thy
src/HOL/Analysis/Gamma_Function.thy
src/HOL/Analysis/Summation_Tests.thy
src/HOL/Library/Predicate_Compile_Quickcheck.thy
src/HOL/Probability/Characteristic_Functions.thy
src/HOL/Probability/Distribution_Functions.thy
src/HOL/Tools/Argo/argo_real.ML
src/HOL/Tools/Argo/argo_sat_solver.ML
src/HOL/Tools/Argo/argo_tactic.ML
src/Pure/General/json.scala
src/Pure/Tools/ci_api.scala
src/Tools/Argo/argo_expr.ML
src/Tools/Argo/argo_thy.ML
--- 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.